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

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 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.

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

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

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

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

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

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

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

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

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

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

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

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.

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

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.

@[simp]

theorem hasFDerivAtFilter_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} {f' : E →L[𝕜] F} {x : E} {L : Filter E} (c : F) : HasFDerivAtFilter (fun (x : E) => f x + c) f' x L ↔ HasFDerivAtFilter f f' x L

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} (c : F) : HasFDerivAtFilter f f' x L → HasFDerivAtFilter (fun (x : E) => f x + c) f' x L

Alias of the reverse direction of hasFDerivAtFilter_add_const_iff.

@[simp]

theorem hasStrictFDerivAt_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} {f' : E →L[𝕜] F} {x : E} (c : F) : HasStrictFDerivAt (fun (x : E) => f x + c) f' x ↔ HasStrictFDerivAt f f' 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} (c : F) : HasStrictFDerivAt f f' x → HasStrictFDerivAt (fun (x : E) => f x + c) f' x

Alias of the reverse direction of hasStrictFDerivAt_add_const_iff.

@[simp]

theorem hasFDerivWithinAt_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} {f' : E →L[𝕜] F} {x : E} {s : Set E} (c : F) : HasFDerivWithinAt (fun (x : E) => f x + c) f' s x ↔ HasFDerivWithinAt f f' s x

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} (c : F) : HasFDerivWithinAt f f' s x → HasFDerivWithinAt (fun (x : E) => f x + c) f' s x

Alias of the reverse direction of hasFDerivWithinAt_add_const_iff.

@[simp]

theorem hasFDerivAt_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} {f' : E →L[𝕜] F} {x : E} (c : F) : HasFDerivAt (fun (x : E) => f x + c) f' x ↔ HasFDerivAt f f' 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} (c : F) : HasFDerivAt f f' x → HasFDerivAt (fun (x : E) => f x + c) f' x

Alias of the reverse direction of hasFDerivAt_add_const_iff.

@[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 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} (c : F) : DifferentiableWithinAt 𝕜 f s x → DifferentiableWithinAt 𝕜 (fun (y : E) => f y + c) s x

Alias of the reverse direction of differentiableWithinAt_add_const_iff.

@[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 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} (c : F) : DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 (fun (y : E) => f y + c) x

Alias of the reverse direction of differentiableAt_add_const_iff.

@[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 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} (c : F) : DifferentiableOn 𝕜 f s → DifferentiableOn 𝕜 (fun (y : E) => f y + c) s

Alias of the reverse direction of differentiableOn_add_const_iff.

@[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 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} (c : F) : Differentiable 𝕜 f → Differentiable 𝕜 fun (y : E) => f y + c

Alias of the reverse direction of differentiable_add_const_iff.

@[simp]

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} (c : F) : fderivWithin 𝕜 (fun (y : E) => f y + c) s x = fderivWithin 𝕜 f s x

@[simp]

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

@[simp]

theorem hasFDerivAtFilter_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} {f' : E →L[𝕜] F} {x : E} {L : Filter E} (c : F) : HasFDerivAtFilter (fun (x : E) => c + f x) f' x L ↔ HasFDerivAtFilter f f' x L

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} (c : F) : HasFDerivAtFilter f f' x L → HasFDerivAtFilter (fun (x : E) => c + f x) f' x L

Alias of the reverse direction of hasFDerivAtFilter_const_add_iff.

@[simp]

theorem hasStrictFDerivAt_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} {f' : E →L[𝕜] F} {x : E} (c : F) : HasStrictFDerivAt (fun (x : E) => c + f x) f' x ↔ HasStrictFDerivAt f 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} (c : F) : HasStrictFDerivAt f f' x → HasStrictFDerivAt (fun (x : E) => c + f x) f' x

Alias of the reverse direction of hasStrictFDerivAt_const_add_iff.

@[simp]

theorem hasFDerivWithinAt_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} {f' : E →L[𝕜] F} {x : E} {s : Set E} (c : F) : HasFDerivWithinAt (fun (x : E) => c + f x) f' s x ↔ HasFDerivWithinAt f f' s x

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} (c : F) : HasFDerivWithinAt f f' s x → HasFDerivWithinAt (fun (x : E) => c + f x) f' s x

Alias of the reverse direction of hasFDerivWithinAt_const_add_iff.

@[simp]

theorem hasFDerivAt_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} {f' : E →L[𝕜] F} {x : E} (c : F) : HasFDerivAt (fun (x : E) => c + f x) f' x ↔ HasFDerivAt f f' 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} (c : F) : HasFDerivAt f f' x → HasFDerivAt (fun (x : E) => c + f x) f' x

Alias of the reverse direction of hasFDerivAt_const_add_iff.

@[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 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} (c : F) : DifferentiableWithinAt 𝕜 f s x → DifferentiableWithinAt 𝕜 (fun (y : E) => c + f y) s x

Alias of the reverse direction of differentiableWithinAt_const_add_iff.

@[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 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} (c : F) : DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 (fun (y : E) => c + f y) x

Alias of the reverse direction of differentiableAt_const_add_iff.

@[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 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} (c : F) : DifferentiableOn 𝕜 f s → DifferentiableOn 𝕜 (fun (y : E) => c + f y) s

Alias of the reverse direction of differentiableOn_const_add_iff.

@[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 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} (c : F) : Differentiable 𝕜 f → Differentiable 𝕜 fun (y : E) => c + f y

Alias of the reverse direction of differentiable_const_add_iff.

@[simp]

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} (c : F) : fderivWithin 𝕜 (fun (y : E) => c + f y) s x = fderivWithin 𝕜 f s x

@[simp]

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

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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.

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

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.

@[simp]

theorem hasFDerivAtFilter_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} {f' : E →L[𝕜] F} {x : E} {L : Filter E} (c : F) : HasFDerivAtFilter (fun (x : E) => f x - c) f' x L ↔ HasFDerivAtFilter f f' x L

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} (c : F) : HasFDerivAtFilter f f' x L → HasFDerivAtFilter (fun (x : E) => f x - c) f' x L

Alias of the reverse direction of hasFDerivAtFilter_sub_const_iff.

@[simp]

theorem hasStrictFDerivAt_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} {f' : E →L[𝕜] F} {x : E} (c : F) : HasStrictFDerivAt (fun (x : E) => f x - c) f' x ↔ HasStrictFDerivAt f f' 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} (c : F) : HasStrictFDerivAt f f' x → HasStrictFDerivAt (fun (x : E) => f x - c) f' x

Alias of the reverse direction of hasStrictFDerivAt_sub_const_iff.

@[simp]

theorem hasFDerivWithinAt_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} {f' : E →L[𝕜] F} {x : E} {s : Set E} (c : F) : HasFDerivWithinAt (fun (x : E) => f x - c) f' s x ↔ HasFDerivWithinAt f f' s x

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} (c : F) : HasFDerivWithinAt f f' s x → HasFDerivWithinAt (fun (x : E) => f x - c) f' s x

Alias of the reverse direction of hasFDerivWithinAt_sub_const_iff.

@[simp]

theorem hasFDerivAt_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} {f' : E →L[𝕜] F} {x : E} (c : F) : HasFDerivAt (fun (x : E) => f x - c) f' x ↔ HasFDerivAt f f' 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} (c : F) : HasFDerivAt f f' x → HasFDerivAt (fun (x : E) => f x - c) f' x

Alias of the reverse direction of hasFDerivAt_sub_const_iff.

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

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

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

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} (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 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 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 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

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

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

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

Derivative of the composition with a translation

theorem hasFDerivWithinAt_comp_add_left {𝕜 : 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} (a : E) : HasFDerivWithinAt (fun (x : E) => f (a + x)) f' s x ↔ HasFDerivWithinAt f f' (a +ᵥ s) (a + x)

theorem differentiableWithinAt_comp_add_left {𝕜 : 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} (a : E) : DifferentiableWithinAt 𝕜 (fun (x : E) => f (a + x)) s x ↔ DifferentiableWithinAt 𝕜 f (a +ᵥ s) (a + x)

theorem fderivWithin_comp_add_left {𝕜 : 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} (a : E) : fderivWithin 𝕜 (fun (x : E) => f (a + x)) s x = fderivWithin 𝕜 f (a +ᵥ s) (a + x)

theorem hasFDerivWithinAt_comp_add_right {𝕜 : 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} (a : E) : HasFDerivWithinAt (fun (x : E) => f (x + a)) f' s x ↔ HasFDerivWithinAt f f' (a +ᵥ s) (x + a)

theorem differentiableWithinAt_comp_add_right {𝕜 : 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} (a : E) : DifferentiableWithinAt 𝕜 (fun (x : E) => f (x + a)) s x ↔ DifferentiableWithinAt 𝕜 f (a +ᵥ s) (x + a)

theorem fderivWithin_comp_add_right {𝕜 : 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} (a : E) : fderivWithin 𝕜 (fun (x : E) => f (x + a)) s x = fderivWithin 𝕜 f (a +ᵥ s) (x + a)

theorem hasFDerivAt_comp_add_right {𝕜 : 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} (a : E) : HasFDerivAt (fun (x : E) => f (x + a)) f' x ↔ HasFDerivAt f f' (x + a)

theorem differentiableAt_comp_add_right {𝕜 : 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} (a : E) : DifferentiableAt 𝕜 (fun (x : E) => f (x + a)) x ↔ DifferentiableAt 𝕜 f (x + a)

theorem fderiv_comp_add_right {𝕜 : 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} (a : E) : fderiv 𝕜 (fun (x : E) => f (x + a)) x = fderiv 𝕜 f (x + a)

theorem hasFDerivAt_comp_add_left {𝕜 : 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} (a : E) : HasFDerivAt (fun (x : E) => f (a + x)) f' x ↔ HasFDerivAt f f' (a + x)

theorem differentiableAt_comp_add_left {𝕜 : 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} (a : E) : DifferentiableAt 𝕜 (fun (x : E) => f (a + x)) x ↔ DifferentiableAt 𝕜 f (a + x)

theorem fderiv_comp_add_left {𝕜 : 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} (a : E) : fderiv 𝕜 (fun (x : E) => f (a + x)) x = fderiv 𝕜 f (a + x)

theorem hasFDerivWithinAt_comp_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} (a : E) : HasFDerivWithinAt (fun (x : E) => f (x - a)) f' s x ↔ HasFDerivWithinAt f f' (-a +ᵥ s) (x - a)

theorem differentiableWithinAt_comp_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} (a : E) : DifferentiableWithinAt 𝕜 (fun (x : E) => f (x - a)) s x ↔ DifferentiableWithinAt 𝕜 f (-a +ᵥ s) (x - a)

theorem fderivWithin_comp_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} (a : E) : fderivWithin 𝕜 (fun (x : E) => f (x - a)) s x = fderivWithin 𝕜 f (-a +ᵥ s) (x - a)

theorem hasFDerivAt_comp_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} (a : E) : HasFDerivAt (fun (x : E) => f (x - a)) f' x ↔ HasFDerivAt f f' (x - a)

theorem differentiableAt_comp_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} (a : E) : DifferentiableAt 𝕜 (fun (x : E) => f (x - a)) x ↔ DifferentiableAt 𝕜 f (x - a)

theorem fderiv_comp_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} (a : E) : fderiv 𝕜 (fun (x : E) => f (x - a)) x = fderiv 𝕜 f (x - a)