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

sum of finitely many functions
multiplication of a function by a scalar constant
negative of a function
subtraction of two functions

Derivative of a function multiplied by a constant #

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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 𝕜 (c • f) s x = c • fderivWithin 𝕜 f s x

Version of fderivWithin_const_smul written with c • f instead of fun y ↦ c • f y.

source

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

source

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 𝕜 (c • f) x = c • fderiv 𝕜 f x

Version of fderiv_const_smul written with c • f instead of fun y ↦ c • f y.

Derivative of the sum of two functions #

source

theorem HasStrictFDerivAt.add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {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

source

theorem HasFDerivAtFilter.add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {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

source

theorem HasFDerivWithinAt.add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {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

source

theorem HasFDerivAt.add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {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

source

theorem DifferentiableWithinAt.add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {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

source

@[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 g : E → F} {x : E} (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :

DifferentiableAt 𝕜 (fun (y : E) => f y + g y) x

source

theorem DifferentiableOn.add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {s : Set E} (hf : DifferentiableOn 𝕜 f s) (hg : DifferentiableOn 𝕜 g s) :

DifferentiableOn 𝕜 (fun (y : E) => f y + g y) s

source

@[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 g : E → F} (hf : Differentiable 𝕜 f) (hg : Differentiable 𝕜 g) :

Differentiable 𝕜 fun (y : E) => f y + g y

source

theorem fderivWithin_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {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

source

theorem fderivWithin_add' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {x : E} {s : Set E} (hxs : UniqueDiffWithinAt 𝕜 s x) (hf : DifferentiableWithinAt 𝕜 f s x) (hg : DifferentiableWithinAt 𝕜 g s x) :

fderivWithin 𝕜 (f + g) s x = fderivWithin 𝕜 f s x + fderivWithin 𝕜 g s x

Version of fderivWithin_add where the function is written as f + g instead of fun y ↦ f y + g y.

source

theorem fderiv_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {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

source

theorem fderiv_add' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {x : E} (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :

fderiv 𝕜 (f + g) x = fderiv 𝕜 f x + fderiv 𝕜 g x

Version of fderiv_add where the function is written as f + g instead of fun y ↦ f y + g y.

source

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

source

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

source

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

source

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

source

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

source

@[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

source

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

source

@[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

source

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

source

@[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

source

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

source

@[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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

@[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

source

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

source

@[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

source

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

source

@[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

source

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

source

@[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

source

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

source

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 #

source

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

source

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

source

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

source

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

source

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

source

@[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

source

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

source

@[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

source

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

source

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 #

source

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

source

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

source

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

source

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

source

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

source

@[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

source

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

source

@[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

source

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

source

@[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

source

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

source

@[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

source

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

source

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 𝕜 (-f) s x = -fderivWithin 𝕜 f s x

Version of fderivWithin_neg where the function is written -f instead of fun y ↦ - f y.

source

@[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

source

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 𝕜 (-f) x = -fderiv 𝕜 f x

Version of fderiv_neg where the function is written -f instead of fun y ↦ - f y.

Derivative of the difference of two functions #

source

theorem HasStrictFDerivAt.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {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

source

theorem HasFDerivAtFilter.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {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

source

theorem HasFDerivWithinAt.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {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

source

theorem HasFDerivAt.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {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

source

theorem DifferentiableWithinAt.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {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

source

@[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 g : E → F} {x : E} (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :

DifferentiableAt 𝕜 (fun (y : E) => f y - g y) x

source

@[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 g : E → F} {x : E} (hg : DifferentiableAt 𝕜 g x) :

DifferentiableAt 𝕜 (fun (y : E) => f y + g y) x ↔ DifferentiableAt 𝕜 f x

source

@[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 g : E → F} {x : E} (hg : DifferentiableAt 𝕜 f x) :

DifferentiableAt 𝕜 (fun (y : E) => f y + g y) x ↔ DifferentiableAt 𝕜 g x

source

@[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 g : E → F} {x : E} (hg : DifferentiableAt 𝕜 g x) :

DifferentiableAt 𝕜 (fun (y : E) => f y - g y) x ↔ DifferentiableAt 𝕜 f x

source

@[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 g : E → F} {x : E} (hg : DifferentiableAt 𝕜 f x) :

DifferentiableAt 𝕜 (fun (y : E) => f y - g y) x ↔ DifferentiableAt 𝕜 g x

source

theorem DifferentiableOn.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {s : Set E} (hf : DifferentiableOn 𝕜 f s) (hg : DifferentiableOn 𝕜 g s) :

DifferentiableOn 𝕜 (fun (y : E) => f y - g y) s

source

@[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 g : E → F} {s : Set E} (hg : DifferentiableOn 𝕜 g s) :

DifferentiableOn 𝕜 (fun (y : E) => f y + g y) s ↔ DifferentiableOn 𝕜 f s

source

@[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 g : E → F} {s : Set E} (hg : DifferentiableOn 𝕜 f s) :

DifferentiableOn 𝕜 (fun (y : E) => f y + g y) s ↔ DifferentiableOn 𝕜 g s

source

@[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 g : E → F} {s : Set E} (hg : DifferentiableOn 𝕜 g s) :

DifferentiableOn 𝕜 (fun (y : E) => f y - g y) s ↔ DifferentiableOn 𝕜 f s

source

@[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 g : E → F} {s : Set E} (hg : DifferentiableOn 𝕜 f s) :

DifferentiableOn 𝕜 (fun (y : E) => f y - g y) s ↔ DifferentiableOn 𝕜 g s

source

@[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 g : E → F} (hf : Differentiable 𝕜 f) (hg : Differentiable 𝕜 g) :

Differentiable 𝕜 fun (y : E) => f y - g y

source

@[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 g : E → F} (hg : Differentiable 𝕜 g) :

(Differentiable 𝕜 fun (y : E) => f y + g y) ↔ Differentiable 𝕜 f

source

@[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 g : E → F} (hg : Differentiable 𝕜 f) :

(Differentiable 𝕜 fun (y : E) => f y + g y) ↔ Differentiable 𝕜 g

source

@[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 g : E → F} (hg : Differentiable 𝕜 g) :

(Differentiable 𝕜 fun (y : E) => f y - g y) ↔ Differentiable 𝕜 f

source

@[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 g : E → F} (hg : Differentiable 𝕜 f) :

(Differentiable 𝕜 fun (y : E) => f y - g y) ↔ Differentiable 𝕜 g

source

theorem fderivWithin_sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {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

source

theorem fderivWithin_sub' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {x : E} {s : Set E} (hxs : UniqueDiffWithinAt 𝕜 s x) (hf : DifferentiableWithinAt 𝕜 f s x) (hg : DifferentiableWithinAt 𝕜 g s x) :

fderivWithin 𝕜 (f - g) s x = fderivWithin 𝕜 f s x - fderivWithin 𝕜 g s x

Version of fderivWithin_sub where the function is written as f - g instead of fun y ↦ f y - g y.

source

theorem fderiv_sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {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

source

theorem fderiv_sub' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {x : E} (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :

fderiv 𝕜 (f - g) x = fderiv 𝕜 f x - fderiv 𝕜 g x

Version of fderiv_sub where the function is written as f - g instead of fun y ↦ f y - g y.

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

@[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

source

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

source

@[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

source

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

source

@[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

source

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

source

@[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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

@[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

source

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

source

@[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

source

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

source

@[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

source

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

source

@[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

source

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

source

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

HepLean Documentation

Mathlib.Analysis.Calculus.FDeriv.Add

Additive operations on derivatives #

Derivative of a function multiplied by a constant #

Derivative of the sum of two functions #

Derivative of a finite sum of functions #

Derivative of the negative of a function #

Derivative of the difference of two functions #