Documentation

Mathlib.Analysis.Calculus.FDeriv.Add

Additive operations on derivatives #

For detailed documentation of the FrΓ©chet derivative, see the module docstring of Analysis/Calculus/FDeriv/Basic.lean.

This file contains the usual formulas (and existence assertions) for the derivative of

Derivative of a function multiplied by a constant #

theorem HasStrictFDerivAt.const_smul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} {R : Type u_4} [Semiring R] [Module R F] [SMulCommClass π•œ R F] [ContinuousConstSMul R F] (h : HasStrictFDerivAt f f' x) (c : R) :
HasStrictFDerivAt (fun (x : E) => c β€’ f x) (c β€’ f') x
theorem HasFDerivAtFilter.const_smul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} {L : Filter E} {R : Type u_4} [Semiring R] [Module R F] [SMulCommClass π•œ R F] [ContinuousConstSMul R F] (h : HasFDerivAtFilter f f' x L) (c : R) :
HasFDerivAtFilter (fun (x : E) => c β€’ f x) (c β€’ f') x L
theorem HasFDerivWithinAt.const_smul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} {s : Set E} {R : Type u_4} [Semiring R] [Module R F] [SMulCommClass π•œ R F] [ContinuousConstSMul R F] (h : HasFDerivWithinAt f f' s x) (c : R) :
HasFDerivWithinAt (fun (x : E) => c β€’ f x) (c β€’ f') s x
theorem HasFDerivAt.const_smul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} {R : Type u_4} [Semiring R] [Module R F] [SMulCommClass π•œ R F] [ContinuousConstSMul R F] (h : HasFDerivAt f f' x) (c : R) :
HasFDerivAt (fun (x : E) => c β€’ f x) (c β€’ f') x
theorem DifferentiableWithinAt.const_smul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {s : Set E} {R : Type u_4} [Semiring R] [Module R F] [SMulCommClass π•œ R F] [ContinuousConstSMul R F] (h : DifferentiableWithinAt π•œ f s x) (c : R) :
DifferentiableWithinAt π•œ (fun (y : E) => c β€’ f y) s x
theorem DifferentiableAt.const_smul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {R : Type u_4} [Semiring R] [Module R F] [SMulCommClass π•œ R F] [ContinuousConstSMul R F] (h : DifferentiableAt π•œ f x) (c : R) :
DifferentiableAt π•œ (fun (y : E) => c β€’ f y) x
theorem DifferentiableOn.const_smul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {s : Set E} {R : Type u_4} [Semiring R] [Module R F] [SMulCommClass π•œ R F] [ContinuousConstSMul R F] (h : DifferentiableOn π•œ f s) (c : R) :
DifferentiableOn π•œ (fun (y : E) => c β€’ f y) s
theorem Differentiable.const_smul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {R : Type u_4} [Semiring R] [Module R F] [SMulCommClass π•œ R F] [ContinuousConstSMul R F] (h : Differentiable π•œ f) (c : R) :
Differentiable π•œ fun (y : E) => c β€’ f y
theorem fderivWithin_const_smul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {s : Set E} {R : Type u_4} [Semiring R] [Module R F] [SMulCommClass π•œ R F] [ContinuousConstSMul R F] (hxs : UniqueDiffWithinAt π•œ s x) (h : DifferentiableWithinAt π•œ f s x) (c : R) :
fderivWithin π•œ (fun (y : E) => c β€’ f y) s x = c β€’ fderivWithin π•œ f s x
theorem fderiv_const_smul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {R : Type u_4} [Semiring R] [Module R F] [SMulCommClass π•œ R F] [ContinuousConstSMul R F] (h : DifferentiableAt π•œ f x) (c : R) :
fderiv π•œ (fun (y : E) => c β€’ f y) x = c β€’ fderiv π•œ f x

Derivative of the sum of two functions #

theorem HasStrictFDerivAt.add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} {f' : E β†’L[π•œ] F} {g' : E β†’L[π•œ] F} {x : E} (hf : HasStrictFDerivAt f f' x) (hg : HasStrictFDerivAt g g' x) :
HasStrictFDerivAt (fun (y : E) => f y + g y) (f' + g') x
theorem HasFDerivAtFilter.add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} {f' : E β†’L[π•œ] F} {g' : E β†’L[π•œ] F} {x : E} {L : Filter E} (hf : HasFDerivAtFilter f f' x L) (hg : HasFDerivAtFilter g g' x L) :
HasFDerivAtFilter (fun (y : E) => f y + g y) (f' + g') x L
theorem HasFDerivWithinAt.add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} {f' : E β†’L[π•œ] F} {g' : E β†’L[π•œ] F} {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) (hg : HasFDerivWithinAt g g' s x) :
HasFDerivWithinAt (fun (y : E) => f y + g y) (f' + g') s x
theorem HasFDerivAt.add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} {f' : E β†’L[π•œ] F} {g' : E β†’L[π•œ] F} {x : E} (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) :
HasFDerivAt (fun (x : E) => f x + g x) (f' + g') x
theorem DifferentiableWithinAt.add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} {x : E} {s : Set E} (hf : DifferentiableWithinAt π•œ f s x) (hg : DifferentiableWithinAt π•œ g s x) :
DifferentiableWithinAt π•œ (fun (y : E) => f y + g y) s x
@[simp]
theorem DifferentiableAt.add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} {x : E} (hf : DifferentiableAt π•œ f x) (hg : DifferentiableAt π•œ g x) :
DifferentiableAt π•œ (fun (y : E) => f y + g y) x
theorem DifferentiableOn.add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} {s : Set E} (hf : DifferentiableOn π•œ f s) (hg : DifferentiableOn π•œ g s) :
DifferentiableOn π•œ (fun (y : E) => f y + g y) s
@[simp]
theorem Differentiable.add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} (hf : Differentiable π•œ f) (hg : Differentiable π•œ g) :
Differentiable π•œ fun (y : E) => f y + g y
theorem fderivWithin_add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} {x : E} {s : Set E} (hxs : UniqueDiffWithinAt π•œ s x) (hf : DifferentiableWithinAt π•œ f s x) (hg : DifferentiableWithinAt π•œ g s x) :
fderivWithin π•œ (fun (y : E) => f y + g y) s x = fderivWithin π•œ f s x + fderivWithin π•œ g s x
theorem fderiv_add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} {x : E} (hf : DifferentiableAt π•œ f x) (hg : DifferentiableAt π•œ g x) :
fderiv π•œ (fun (y : E) => f y + g y) x = fderiv π•œ f x + fderiv π•œ g x
theorem HasStrictFDerivAt.add_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} (hf : HasStrictFDerivAt f f' x) (c : F) :
HasStrictFDerivAt (fun (y : E) => f y + c) f' x
theorem HasFDerivAtFilter.add_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} {L : Filter E} (hf : HasFDerivAtFilter f f' x L) (c : F) :
HasFDerivAtFilter (fun (y : E) => f y + c) f' x L
theorem HasFDerivWithinAt.add_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) (c : F) :
HasFDerivWithinAt (fun (y : E) => f y + c) f' s x
theorem HasFDerivAt.add_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} (hf : HasFDerivAt f f' x) (c : F) :
HasFDerivAt (fun (x : E) => f x + c) f' x
theorem DifferentiableWithinAt.add_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {s : Set E} (hf : DifferentiableWithinAt π•œ f s x) (c : F) :
DifferentiableWithinAt π•œ (fun (y : E) => f y + c) s x
@[simp]
theorem differentiableWithinAt_add_const_iff {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {s : Set E} (c : F) :
DifferentiableWithinAt π•œ (fun (y : E) => f y + c) s x ↔ DifferentiableWithinAt π•œ f s x
theorem DifferentiableAt.add_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} (hf : DifferentiableAt π•œ f x) (c : F) :
DifferentiableAt π•œ (fun (y : E) => f y + c) x
@[simp]
theorem differentiableAt_add_const_iff {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} (c : F) :
DifferentiableAt π•œ (fun (y : E) => f y + c) x ↔ DifferentiableAt π•œ f x
theorem DifferentiableOn.add_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {s : Set E} (hf : DifferentiableOn π•œ f s) (c : F) :
DifferentiableOn π•œ (fun (y : E) => f y + c) s
@[simp]
theorem differentiableOn_add_const_iff {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {s : Set E} (c : F) :
DifferentiableOn π•œ (fun (y : E) => f y + c) s ↔ DifferentiableOn π•œ f s
theorem Differentiable.add_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} (hf : Differentiable π•œ f) (c : F) :
Differentiable π•œ fun (y : E) => f y + c
@[simp]
theorem differentiable_add_const_iff {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} (c : F) :
(Differentiable π•œ fun (y : E) => f y + c) ↔ Differentiable π•œ f
theorem fderivWithin_add_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {s : Set E} (hxs : UniqueDiffWithinAt π•œ s x) (c : F) :
fderivWithin π•œ (fun (y : E) => f y + c) s x = fderivWithin π•œ f s x
theorem fderiv_add_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} (c : F) :
fderiv π•œ (fun (y : E) => f y + c) x = fderiv π•œ f x
theorem HasStrictFDerivAt.const_add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} (hf : HasStrictFDerivAt f f' x) (c : F) :
HasStrictFDerivAt (fun (y : E) => c + f y) f' x
theorem HasFDerivAtFilter.const_add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} {L : Filter E} (hf : HasFDerivAtFilter f f' x L) (c : F) :
HasFDerivAtFilter (fun (y : E) => c + f y) f' x L
theorem HasFDerivWithinAt.const_add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) (c : F) :
HasFDerivWithinAt (fun (y : E) => c + f y) f' s x
theorem HasFDerivAt.const_add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} (hf : HasFDerivAt f f' x) (c : F) :
HasFDerivAt (fun (x : E) => c + f x) f' x
theorem DifferentiableWithinAt.const_add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {s : Set E} (hf : DifferentiableWithinAt π•œ f s x) (c : F) :
DifferentiableWithinAt π•œ (fun (y : E) => c + f y) s x
@[simp]
theorem differentiableWithinAt_const_add_iff {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {s : Set E} (c : F) :
DifferentiableWithinAt π•œ (fun (y : E) => c + f y) s x ↔ DifferentiableWithinAt π•œ f s x
theorem DifferentiableAt.const_add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} (hf : DifferentiableAt π•œ f x) (c : F) :
DifferentiableAt π•œ (fun (y : E) => c + f y) x
@[simp]
theorem differentiableAt_const_add_iff {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} (c : F) :
DifferentiableAt π•œ (fun (y : E) => c + f y) x ↔ DifferentiableAt π•œ f x
theorem DifferentiableOn.const_add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {s : Set E} (hf : DifferentiableOn π•œ f s) (c : F) :
DifferentiableOn π•œ (fun (y : E) => c + f y) s
@[simp]
theorem differentiableOn_const_add_iff {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {s : Set E} (c : F) :
DifferentiableOn π•œ (fun (y : E) => c + f y) s ↔ DifferentiableOn π•œ f s
theorem Differentiable.const_add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} (hf : Differentiable π•œ f) (c : F) :
Differentiable π•œ fun (y : E) => c + f y
@[simp]
theorem differentiable_const_add_iff {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} (c : F) :
(Differentiable π•œ fun (y : E) => c + f y) ↔ Differentiable π•œ f
theorem fderivWithin_const_add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {s : Set E} (hxs : UniqueDiffWithinAt π•œ s x) (c : F) :
fderivWithin π•œ (fun (y : E) => c + f y) s x = fderivWithin π•œ f s x
theorem fderiv_const_add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} (c : F) :
fderiv π•œ (fun (y : E) => c + f y) x = fderiv π•œ f x

Derivative of a finite sum of functions #

theorem HasStrictFDerivAt.sum {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {x : E} {ΞΉ : Type u_4} {u : Finset ΞΉ} {A : ΞΉ β†’ E β†’ F} {A' : ΞΉ β†’ E β†’L[π•œ] F} (h : βˆ€ i ∈ u, HasStrictFDerivAt (A i) (A' i) x) :
HasStrictFDerivAt (fun (y : E) => βˆ‘ i ∈ u, A i y) (βˆ‘ i ∈ u, A' i) x
theorem HasFDerivAtFilter.sum {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {x : E} {L : Filter E} {ΞΉ : Type u_4} {u : Finset ΞΉ} {A : ΞΉ β†’ E β†’ F} {A' : ΞΉ β†’ E β†’L[π•œ] F} (h : βˆ€ i ∈ u, HasFDerivAtFilter (A i) (A' i) x L) :
HasFDerivAtFilter (fun (y : E) => βˆ‘ i ∈ u, A i y) (βˆ‘ i ∈ u, A' i) x L
theorem HasFDerivWithinAt.sum {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {x : E} {s : Set E} {ΞΉ : Type u_4} {u : Finset ΞΉ} {A : ΞΉ β†’ E β†’ F} {A' : ΞΉ β†’ E β†’L[π•œ] F} (h : βˆ€ i ∈ u, HasFDerivWithinAt (A i) (A' i) s x) :
HasFDerivWithinAt (fun (y : E) => βˆ‘ i ∈ u, A i y) (βˆ‘ i ∈ u, A' i) s x
theorem HasFDerivAt.sum {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {x : E} {ΞΉ : Type u_4} {u : Finset ΞΉ} {A : ΞΉ β†’ E β†’ F} {A' : ΞΉ β†’ E β†’L[π•œ] F} (h : βˆ€ i ∈ u, HasFDerivAt (A i) (A' i) x) :
HasFDerivAt (fun (y : E) => βˆ‘ i ∈ u, A i y) (βˆ‘ i ∈ u, A' i) x
theorem DifferentiableWithinAt.sum {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {x : E} {s : Set E} {ΞΉ : Type u_4} {u : Finset ΞΉ} {A : ΞΉ β†’ E β†’ F} (h : βˆ€ i ∈ u, DifferentiableWithinAt π•œ (A i) s x) :
DifferentiableWithinAt π•œ (fun (y : E) => βˆ‘ i ∈ u, A i y) s x
@[simp]
theorem DifferentiableAt.sum {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {x : E} {ΞΉ : Type u_4} {u : Finset ΞΉ} {A : ΞΉ β†’ E β†’ F} (h : βˆ€ i ∈ u, DifferentiableAt π•œ (A i) x) :
DifferentiableAt π•œ (fun (y : E) => βˆ‘ i ∈ u, A i y) x
theorem DifferentiableOn.sum {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {ΞΉ : Type u_4} {u : Finset ΞΉ} {A : ΞΉ β†’ E β†’ F} (h : βˆ€ i ∈ u, DifferentiableOn π•œ (A i) s) :
DifferentiableOn π•œ (fun (y : E) => βˆ‘ i ∈ u, A i y) s
@[simp]
theorem Differentiable.sum {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {ΞΉ : Type u_4} {u : Finset ΞΉ} {A : ΞΉ β†’ E β†’ F} (h : βˆ€ i ∈ u, Differentiable π•œ (A i)) :
Differentiable π•œ fun (y : E) => βˆ‘ i ∈ u, A i y
theorem fderivWithin_sum {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {x : E} {s : Set E} {ΞΉ : Type u_4} {u : Finset ΞΉ} {A : ΞΉ β†’ E β†’ F} (hxs : UniqueDiffWithinAt π•œ s x) (h : βˆ€ i ∈ u, DifferentiableWithinAt π•œ (A i) s x) :
fderivWithin π•œ (fun (y : E) => βˆ‘ i ∈ u, A i y) s x = βˆ‘ i ∈ u, fderivWithin π•œ (A i) s x
theorem fderiv_sum {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {x : E} {ΞΉ : Type u_4} {u : Finset ΞΉ} {A : ΞΉ β†’ E β†’ F} (h : βˆ€ i ∈ u, DifferentiableAt π•œ (A i) x) :
fderiv π•œ (fun (y : E) => βˆ‘ i ∈ u, A i y) x = βˆ‘ i ∈ u, fderiv π•œ (A i) x

Derivative of the negative of a function #

theorem HasStrictFDerivAt.neg {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} (h : HasStrictFDerivAt f f' x) :
HasStrictFDerivAt (fun (x : E) => -f x) (-f') x
theorem HasFDerivAtFilter.neg {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} {L : Filter E} (h : HasFDerivAtFilter f f' x L) :
HasFDerivAtFilter (fun (x : E) => -f x) (-f') x L
theorem HasFDerivWithinAt.neg {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} {s : Set E} (h : HasFDerivWithinAt f f' s x) :
HasFDerivWithinAt (fun (x : E) => -f x) (-f') s x
theorem HasFDerivAt.neg {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} (h : HasFDerivAt f f' x) :
HasFDerivAt (fun (x : E) => -f x) (-f') x
theorem DifferentiableWithinAt.neg {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {s : Set E} (h : DifferentiableWithinAt π•œ f s x) :
DifferentiableWithinAt π•œ (fun (y : E) => -f y) s x
@[simp]
theorem differentiableWithinAt_neg_iff {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {s : Set E} :
DifferentiableWithinAt π•œ (fun (y : E) => -f y) s x ↔ DifferentiableWithinAt π•œ f s x
theorem DifferentiableAt.neg {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} (h : DifferentiableAt π•œ f x) :
DifferentiableAt π•œ (fun (y : E) => -f y) x
@[simp]
theorem differentiableAt_neg_iff {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} :
DifferentiableAt π•œ (fun (y : E) => -f y) x ↔ DifferentiableAt π•œ f x
theorem DifferentiableOn.neg {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {s : Set E} (h : DifferentiableOn π•œ f s) :
DifferentiableOn π•œ (fun (y : E) => -f y) s
@[simp]
theorem differentiableOn_neg_iff {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {s : Set E} :
DifferentiableOn π•œ (fun (y : E) => -f y) s ↔ DifferentiableOn π•œ f s
theorem Differentiable.neg {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} (h : Differentiable π•œ f) :
Differentiable π•œ fun (y : E) => -f y
@[simp]
theorem differentiable_neg_iff {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} :
(Differentiable π•œ fun (y : E) => -f y) ↔ Differentiable π•œ f
theorem fderivWithin_neg {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {s : Set E} (hxs : UniqueDiffWithinAt π•œ s x) :
fderivWithin π•œ (fun (y : E) => -f y) s x = -fderivWithin π•œ f s x
@[simp]
theorem fderiv_neg {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} :
fderiv π•œ (fun (y : E) => -f y) x = -fderiv π•œ f x

Derivative of the difference of two functions #

theorem HasStrictFDerivAt.sub {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} {f' : E β†’L[π•œ] F} {g' : E β†’L[π•œ] F} {x : E} (hf : HasStrictFDerivAt f f' x) (hg : HasStrictFDerivAt g g' x) :
HasStrictFDerivAt (fun (x : E) => f x - g x) (f' - g') x
theorem HasFDerivAtFilter.sub {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} {f' : E β†’L[π•œ] F} {g' : E β†’L[π•œ] F} {x : E} {L : Filter E} (hf : HasFDerivAtFilter f f' x L) (hg : HasFDerivAtFilter g g' x L) :
HasFDerivAtFilter (fun (x : E) => f x - g x) (f' - g') x L
theorem HasFDerivWithinAt.sub {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} {f' : E β†’L[π•œ] F} {g' : E β†’L[π•œ] F} {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) (hg : HasFDerivWithinAt g g' s x) :
HasFDerivWithinAt (fun (x : E) => f x - g x) (f' - g') s x
theorem HasFDerivAt.sub {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} {f' : E β†’L[π•œ] F} {g' : E β†’L[π•œ] F} {x : E} (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) :
HasFDerivAt (fun (x : E) => f x - g x) (f' - g') x
theorem DifferentiableWithinAt.sub {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} {x : E} {s : Set E} (hf : DifferentiableWithinAt π•œ f s x) (hg : DifferentiableWithinAt π•œ g s x) :
DifferentiableWithinAt π•œ (fun (y : E) => f y - g y) s x
@[simp]
theorem DifferentiableAt.sub {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} {x : E} (hf : DifferentiableAt π•œ f x) (hg : DifferentiableAt π•œ g x) :
DifferentiableAt π•œ (fun (y : E) => f y - g y) x
@[simp]
theorem DifferentiableAt.add_iff_left {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} {x : E} (hg : DifferentiableAt π•œ g x) :
DifferentiableAt π•œ (fun (y : E) => f y + g y) x ↔ DifferentiableAt π•œ f x
@[simp]
theorem DifferentiableAt.add_iff_right {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} {x : E} (hg : DifferentiableAt π•œ f x) :
DifferentiableAt π•œ (fun (y : E) => f y + g y) x ↔ DifferentiableAt π•œ g x
@[simp]
theorem DifferentiableAt.sub_iff_left {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} {x : E} (hg : DifferentiableAt π•œ g x) :
DifferentiableAt π•œ (fun (y : E) => f y - g y) x ↔ DifferentiableAt π•œ f x
@[simp]
theorem DifferentiableAt.sub_iff_right {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} {x : E} (hg : DifferentiableAt π•œ f x) :
DifferentiableAt π•œ (fun (y : E) => f y - g y) x ↔ DifferentiableAt π•œ g x
theorem DifferentiableOn.sub {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} {s : Set E} (hf : DifferentiableOn π•œ f s) (hg : DifferentiableOn π•œ g s) :
DifferentiableOn π•œ (fun (y : E) => f y - g y) s
@[simp]
theorem DifferentiableOn.add_iff_left {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} {s : Set E} (hg : DifferentiableOn π•œ g s) :
DifferentiableOn π•œ (fun (y : E) => f y + g y) s ↔ DifferentiableOn π•œ f s
@[simp]
theorem DifferentiableOn.add_iff_right {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} {s : Set E} (hg : DifferentiableOn π•œ f s) :
DifferentiableOn π•œ (fun (y : E) => f y + g y) s ↔ DifferentiableOn π•œ g s
@[simp]
theorem DifferentiableOn.sub_iff_left {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} {s : Set E} (hg : DifferentiableOn π•œ g s) :
DifferentiableOn π•œ (fun (y : E) => f y - g y) s ↔ DifferentiableOn π•œ f s
@[simp]
theorem DifferentiableOn.sub_iff_right {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} {s : Set E} (hg : DifferentiableOn π•œ f s) :
DifferentiableOn π•œ (fun (y : E) => f y - g y) s ↔ DifferentiableOn π•œ g s
@[simp]
theorem Differentiable.sub {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} (hf : Differentiable π•œ f) (hg : Differentiable π•œ g) :
Differentiable π•œ fun (y : E) => f y - g y
@[simp]
theorem Differentiable.add_iff_left {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} (hg : Differentiable π•œ g) :
(Differentiable π•œ fun (y : E) => f y + g y) ↔ Differentiable π•œ f
@[simp]
theorem Differentiable.add_iff_right {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} (hg : Differentiable π•œ f) :
(Differentiable π•œ fun (y : E) => f y + g y) ↔ Differentiable π•œ g
@[simp]
theorem Differentiable.sub_iff_left {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} (hg : Differentiable π•œ g) :
(Differentiable π•œ fun (y : E) => f y - g y) ↔ Differentiable π•œ f
@[simp]
theorem Differentiable.sub_iff_right {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} (hg : Differentiable π•œ f) :
(Differentiable π•œ fun (y : E) => f y - g y) ↔ Differentiable π•œ g
theorem fderivWithin_sub {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} {x : E} {s : Set E} (hxs : UniqueDiffWithinAt π•œ s x) (hf : DifferentiableWithinAt π•œ f s x) (hg : DifferentiableWithinAt π•œ g s x) :
fderivWithin π•œ (fun (y : E) => f y - g y) s x = fderivWithin π•œ f s x - fderivWithin π•œ g s x
theorem fderiv_sub {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {g : E β†’ F} {x : E} (hf : DifferentiableAt π•œ f x) (hg : DifferentiableAt π•œ g x) :
fderiv π•œ (fun (y : E) => f y - g y) x = fderiv π•œ f x - fderiv π•œ g x
theorem HasStrictFDerivAt.sub_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} (hf : HasStrictFDerivAt f f' x) (c : F) :
HasStrictFDerivAt (fun (x : E) => f x - c) f' x
theorem HasFDerivAtFilter.sub_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} {L : Filter E} (hf : HasFDerivAtFilter f f' x L) (c : F) :
HasFDerivAtFilter (fun (x : E) => f x - c) f' x L
theorem HasFDerivWithinAt.sub_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) (c : F) :
HasFDerivWithinAt (fun (x : E) => f x - c) f' s x
theorem HasFDerivAt.sub_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} (hf : HasFDerivAt f f' x) (c : F) :
HasFDerivAt (fun (x : E) => f x - c) f' x
theorem hasStrictFDerivAt_sub_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {x : F} (c : F) :
HasStrictFDerivAt (fun (x : F) => x - c) (ContinuousLinearMap.id π•œ F) x
theorem hasFDerivAt_sub_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {x : F} (c : F) :
HasFDerivAt (fun (x : F) => x - c) (ContinuousLinearMap.id π•œ F) x
theorem DifferentiableWithinAt.sub_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {s : Set E} (hf : DifferentiableWithinAt π•œ f s x) (c : F) :
DifferentiableWithinAt π•œ (fun (y : E) => f y - c) s x
@[simp]
theorem differentiableWithinAt_sub_const_iff {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {s : Set E} (c : F) :
DifferentiableWithinAt π•œ (fun (y : E) => f y - c) s x ↔ DifferentiableWithinAt π•œ f s x
theorem DifferentiableAt.sub_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} (hf : DifferentiableAt π•œ f x) (c : F) :
DifferentiableAt π•œ (fun (y : E) => f y - c) x
@[deprecated DifferentiableAt.sub_iff_left]
theorem differentiableAt_sub_const_iff {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} (c : F) :
DifferentiableAt π•œ (fun (y : E) => f y - c) x ↔ DifferentiableAt π•œ f x
theorem DifferentiableOn.sub_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {s : Set E} (hf : DifferentiableOn π•œ f s) (c : F) :
DifferentiableOn π•œ (fun (y : E) => f y - c) s
@[deprecated DifferentiableOn.sub_iff_left]
theorem differentiableOn_sub_const_iff {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {s : Set E} (c : F) :
DifferentiableOn π•œ (fun (y : E) => f y - c) s ↔ DifferentiableOn π•œ f s
theorem Differentiable.sub_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} (hf : Differentiable π•œ f) (c : F) :
Differentiable π•œ fun (y : E) => f y - c
@[deprecated Differentiable.sub_iff_left]
theorem differentiable_sub_const_iff {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} (c : F) :
(Differentiable π•œ fun (y : E) => f y - c) ↔ Differentiable π•œ f
theorem fderivWithin_sub_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {s : Set E} (hxs : UniqueDiffWithinAt π•œ s x) (c : F) :
fderivWithin π•œ (fun (y : E) => f y - c) s x = fderivWithin π•œ f s x
theorem fderiv_sub_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} (c : F) :
fderiv π•œ (fun (y : E) => f y - c) x = fderiv π•œ f x
theorem HasStrictFDerivAt.const_sub {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} (hf : HasStrictFDerivAt f f' x) (c : F) :
HasStrictFDerivAt (fun (x : E) => c - f x) (-f') x
theorem HasFDerivAtFilter.const_sub {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} {L : Filter E} (hf : HasFDerivAtFilter f f' x L) (c : F) :
HasFDerivAtFilter (fun (x : E) => c - f x) (-f') x L
theorem HasFDerivWithinAt.const_sub {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) (c : F) :
HasFDerivWithinAt (fun (x : E) => c - f x) (-f') s x
theorem HasFDerivAt.const_sub {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} (hf : HasFDerivAt f f' x) (c : F) :
HasFDerivAt (fun (x : E) => c - f x) (-f') x
theorem DifferentiableWithinAt.const_sub {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {s : Set E} (hf : DifferentiableWithinAt π•œ f s x) (c : F) :
DifferentiableWithinAt π•œ (fun (y : E) => c - f y) s x
@[simp]
theorem differentiableWithinAt_const_sub_iff {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {s : Set E} (c : F) :
DifferentiableWithinAt π•œ (fun (y : E) => c - f y) s x ↔ DifferentiableWithinAt π•œ f s x
theorem DifferentiableAt.const_sub {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} (hf : DifferentiableAt π•œ f x) (c : F) :
DifferentiableAt π•œ (fun (y : E) => c - f y) x
@[deprecated DifferentiableAt.sub_iff_right]
theorem differentiableAt_const_sub_iff {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} (c : F) :
DifferentiableAt π•œ (fun (y : E) => c - f y) x ↔ DifferentiableAt π•œ f x
theorem DifferentiableOn.const_sub {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {s : Set E} (hf : DifferentiableOn π•œ f s) (c : F) :
DifferentiableOn π•œ (fun (y : E) => c - f y) s
@[deprecated DifferentiableOn.sub_iff_right]
theorem differentiableOn_const_sub_iff {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {s : Set E} (c : F) :
DifferentiableOn π•œ (fun (y : E) => c - f y) s ↔ DifferentiableOn π•œ f s
theorem Differentiable.const_sub {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} (hf : Differentiable π•œ f) (c : F) :
Differentiable π•œ fun (y : E) => c - f y
@[deprecated Differentiable.sub_iff_right]
theorem differentiable_const_sub_iff {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} (c : F) :
(Differentiable π•œ fun (y : E) => c - f y) ↔ Differentiable π•œ f
theorem fderivWithin_const_sub {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {s : Set E} (hxs : UniqueDiffWithinAt π•œ s x) (c : F) :
fderivWithin π•œ (fun (y : E) => c - f y) s x = -fderivWithin π•œ f s x
theorem fderiv_const_sub {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} (c : F) :
fderiv π•œ (fun (y : E) => c - f y) x = -fderiv π•œ f x