# 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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {f' : E βL[π] F} {x : E} {R : Type u_6} [] [Module R F] [SMulCommClass π R F] [] (h : ) (c : R) :
HasStrictFDerivAt (fun (x : E) => c β’ f x) (c β’ f') x
theorem HasFDerivAtFilter.const_smul {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {f' : E βL[π] F} {x : E} {L : } {R : Type u_6} [] [Module R F] [SMulCommClass π 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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {f' : E βL[π] F} {x : E} {s : Set E} {R : Type u_6} [] [Module R F] [SMulCommClass π 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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {f' : E βL[π] F} {x : E} {R : Type u_6} [] [Module R F] [SMulCommClass π 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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} {s : Set E} {R : Type u_6} [] [Module R F] [SMulCommClass π 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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} {R : Type u_6} [] [Module R F] [SMulCommClass π R F] [] (h : DifferentiableAt π f x) (c : R) :
DifferentiableAt π (fun (y : E) => c β’ f y) x
theorem DifferentiableOn.const_smul {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {s : Set E} {R : Type u_6} [] [Module R F] [SMulCommClass π R F] [] (h : DifferentiableOn π f s) (c : R) :
DifferentiableOn π (fun (y : E) => c β’ f y) s
theorem Differentiable.const_smul {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {R : Type u_6} [] [Module R F] [SMulCommClass π R F] [] (h : Differentiable π f) (c : R) :
Differentiable π fun (y : E) => c β’ f y
theorem fderivWithin_const_smul {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} {s : Set E} {R : Type u_6} [] [Module R F] [SMulCommClass π R F] [] (hxs : UniqueDiffWithinAt π s x) (h : DifferentiableWithinAt π f s x) (c : R) :
fderivWithin π (fun (y : E) => c β’ f y) s x = c β’ fderivWithin π f s x
theorem fderiv_const_smul {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} {R : Type u_6} [] [Module R F] [SMulCommClass π R F] [] (h : DifferentiableAt π f x) (c : R) :
fderiv π (fun (y : E) => c β’ f y) x = c β’ fderiv π f x

### Derivative of the sum of two functions #

theorem HasStrictFDerivAt.add {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {g : E β F} {f' : E βL[π] F} {g' : E βL[π] F} {x : E} (hf : ) (hg : ) :
HasStrictFDerivAt (fun (y : E) => f y + g y) (f' + g') x
theorem HasFDerivAtFilter.add {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {g : E β F} {f' : E βL[π] F} {g' : E βL[π] F} {x : E} {L : } (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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {g : E β F} {f' : E βL[π] F} {g' : E βL[π] F} {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) (hg : HasFDerivWithinAt g g' s x) :
HasFDerivWithinAt (fun (y : E) => f y + g y) (f' + g') s x
theorem HasFDerivAt.add {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {g : E β F} {f' : E βL[π] F} {g' : E βL[π] F} {x : E} (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) :
HasFDerivAt (fun (x : E) => f x + g x) (f' + g') x
theorem DifferentiableWithinAt.add {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {g : E β F} {x : E} {s : Set E} (hf : DifferentiableWithinAt π f s x) (hg : DifferentiableWithinAt π g s x) :
DifferentiableWithinAt π (fun (y : E) => f y + g y) s x
@[simp]
theorem DifferentiableAt.add {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {g : E β F} {x : E} (hf : DifferentiableAt π f x) (hg : DifferentiableAt π g x) :
DifferentiableAt π (fun (y : E) => f y + g y) x
theorem DifferentiableOn.add {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {g : E β F} {s : Set E} (hf : DifferentiableOn π f s) (hg : DifferentiableOn π g s) :
DifferentiableOn π (fun (y : E) => f y + g y) s
@[simp]
theorem Differentiable.add {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {g : E β F} (hf : Differentiable π f) (hg : Differentiable π g) :
Differentiable π fun (y : E) => f y + g y
theorem fderivWithin_add {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {g : E β F} {x : E} {s : Set E} (hxs : UniqueDiffWithinAt π s x) (hf : DifferentiableWithinAt π f s x) (hg : DifferentiableWithinAt π g s x) :
fderivWithin π (fun (y : E) => f y + g y) s x = fderivWithin π f s x + fderivWithin π g s x
theorem fderiv_add {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {g : E β F} {x : E} (hf : DifferentiableAt π f x) (hg : DifferentiableAt π g x) :
fderiv π (fun (y : E) => f y + g y) x = fderiv π f x + fderiv π g x
theorem HasStrictFDerivAt.add_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {f' : E βL[π] F} {x : E} (hf : ) (c : F) :
HasStrictFDerivAt (fun (y : E) => f y + c) f' x
theorem HasFDerivAtFilter.add_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {f' : E βL[π] F} {x : E} {L : } (hf : HasFDerivAtFilter f f' x L) (c : F) :
HasFDerivAtFilter (fun (y : E) => f y + c) f' x L
theorem HasFDerivWithinAt.add_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {f' : E βL[π] F} {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) (c : F) :
HasFDerivWithinAt (fun (y : E) => f y + c) f' s x
theorem HasFDerivAt.add_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {f' : E βL[π] F} {x : E} (hf : HasFDerivAt f f' x) (c : F) :
HasFDerivAt (fun (x : E) => f x + c) f' x
theorem DifferentiableWithinAt.add_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} {s : Set E} (hf : DifferentiableWithinAt π f s x) (c : F) :
DifferentiableWithinAt π (fun (y : E) => f y + c) s x
@[simp]
theorem differentiableWithinAt_add_const_iff {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} {s : Set E} (c : F) :
DifferentiableWithinAt π (fun (y : E) => f y + c) s x β DifferentiableWithinAt π f s x
theorem DifferentiableAt.add_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} (hf : DifferentiableAt π f x) (c : F) :
DifferentiableAt π (fun (y : E) => f y + c) x
@[simp]
theorem differentiableAt_add_const_iff {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} (c : F) :
DifferentiableAt π (fun (y : E) => f y + c) x β DifferentiableAt π f x
theorem DifferentiableOn.add_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {s : Set E} (hf : DifferentiableOn π f s) (c : F) :
DifferentiableOn π (fun (y : E) => f y + c) s
@[simp]
theorem differentiableOn_add_const_iff {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {s : Set E} (c : F) :
DifferentiableOn π (fun (y : E) => f y + c) s β DifferentiableOn π f s
theorem Differentiable.add_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} (hf : Differentiable π f) (c : F) :
Differentiable π fun (y : E) => f y + c
@[simp]
theorem differentiable_add_const_iff {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} (c : F) :
(Differentiable π fun (y : E) => f y + c) β Differentiable π f
theorem fderivWithin_add_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} {s : Set E} (hxs : UniqueDiffWithinAt π s x) (c : F) :
fderivWithin π (fun (y : E) => f y + c) s x = fderivWithin π f s x
theorem fderiv_add_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} (c : F) :
fderiv π (fun (y : E) => f y + c) x = fderiv π f x
theorem HasStrictFDerivAt.const_add {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {f' : E βL[π] F} {x : E} (hf : ) (c : F) :
HasStrictFDerivAt (fun (y : E) => c + f y) f' x
theorem HasFDerivAtFilter.const_add {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {f' : E βL[π] F} {x : E} {L : } (hf : HasFDerivAtFilter f f' x L) (c : F) :
HasFDerivAtFilter (fun (y : E) => c + f y) f' x L
theorem HasFDerivWithinAt.const_add {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {f' : E βL[π] F} {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) (c : F) :
HasFDerivWithinAt (fun (y : E) => c + f y) f' s x
theorem HasFDerivAt.const_add {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {f' : E βL[π] F} {x : E} (hf : HasFDerivAt f f' x) (c : F) :
HasFDerivAt (fun (x : E) => c + f x) f' x
theorem DifferentiableWithinAt.const_add {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} {s : Set E} (hf : DifferentiableWithinAt π f s x) (c : F) :
DifferentiableWithinAt π (fun (y : E) => c + f y) s x
@[simp]
theorem differentiableWithinAt_const_add_iff {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} {s : Set E} (c : F) :
DifferentiableWithinAt π (fun (y : E) => c + f y) s x β DifferentiableWithinAt π f s x
theorem DifferentiableAt.const_add {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} (hf : DifferentiableAt π f x) (c : F) :
DifferentiableAt π (fun (y : E) => c + f y) x
@[simp]
theorem differentiableAt_const_add_iff {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} (c : F) :
DifferentiableAt π (fun (y : E) => c + f y) x β DifferentiableAt π f x
theorem DifferentiableOn.const_add {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {s : Set E} (hf : DifferentiableOn π f s) (c : F) :
DifferentiableOn π (fun (y : E) => c + f y) s
@[simp]
theorem differentiableOn_const_add_iff {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {s : Set E} (c : F) :
DifferentiableOn π (fun (y : E) => c + f y) s β DifferentiableOn π f s
theorem Differentiable.const_add {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} (hf : Differentiable π f) (c : F) :
Differentiable π fun (y : E) => c + f y
@[simp]
theorem differentiable_const_add_iff {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} (c : F) :
(Differentiable π fun (y : E) => c + f y) β Differentiable π f
theorem fderivWithin_const_add {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} {s : Set E} (hxs : UniqueDiffWithinAt π s x) (c : F) :
fderivWithin π (fun (y : E) => c + f y) s x = fderivWithin π f s x
theorem fderiv_const_add {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {x : E} {ΞΉ : Type u_6} {u : Finset ΞΉ} {A : ΞΉ β E β F} {A' : ΞΉ β E βL[π] F} (h : β i β u, HasStrictFDerivAt (A i) (A' i) x) :
HasStrictFDerivAt (fun (y : E) => u.sum fun (i : ΞΉ) => A i y) (u.sum fun (i : ΞΉ) => A' i) x
theorem HasFDerivAtFilter.sum {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {x : E} {L : } {ΞΉ : Type u_6} {u : Finset ΞΉ} {A : ΞΉ β E β F} {A' : ΞΉ β E βL[π] F} (h : β i β u, HasFDerivAtFilter (A i) (A' i) x L) :
HasFDerivAtFilter (fun (y : E) => u.sum fun (i : ΞΉ) => A i y) (u.sum fun (i : ΞΉ) => A' i) x L
theorem HasFDerivWithinAt.sum {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {x : E} {s : Set E} {ΞΉ : Type u_6} {u : Finset ΞΉ} {A : ΞΉ β E β F} {A' : ΞΉ β E βL[π] F} (h : β i β u, HasFDerivWithinAt (A i) (A' i) s x) :
HasFDerivWithinAt (fun (y : E) => u.sum fun (i : ΞΉ) => A i y) (u.sum fun (i : ΞΉ) => A' i) s x
theorem HasFDerivAt.sum {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {x : E} {ΞΉ : Type u_6} {u : Finset ΞΉ} {A : ΞΉ β E β F} {A' : ΞΉ β E βL[π] F} (h : β i β u, HasFDerivAt (A i) (A' i) x) :
HasFDerivAt (fun (y : E) => u.sum fun (i : ΞΉ) => A i y) (u.sum fun (i : ΞΉ) => A' i) x
theorem DifferentiableWithinAt.sum {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {x : E} {s : Set E} {ΞΉ : Type u_6} {u : Finset ΞΉ} {A : ΞΉ β E β F} (h : β i β u, DifferentiableWithinAt π (A i) s x) :
DifferentiableWithinAt π (fun (y : E) => u.sum fun (i : ΞΉ) => A i y) s x
@[simp]
theorem DifferentiableAt.sum {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {x : E} {ΞΉ : Type u_6} {u : Finset ΞΉ} {A : ΞΉ β E β F} (h : β i β u, DifferentiableAt π (A i) x) :
DifferentiableAt π (fun (y : E) => u.sum fun (i : ΞΉ) => A i y) x
theorem DifferentiableOn.sum {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {s : Set E} {ΞΉ : Type u_6} {u : Finset ΞΉ} {A : ΞΉ β E β F} (h : β i β u, DifferentiableOn π (A i) s) :
DifferentiableOn π (fun (y : E) => u.sum fun (i : ΞΉ) => A i y) s
@[simp]
theorem Differentiable.sum {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {ΞΉ : Type u_6} {u : Finset ΞΉ} {A : ΞΉ β E β F} (h : β i β u, Differentiable π (A i)) :
Differentiable π fun (y : E) => u.sum fun (i : ΞΉ) => A i y
theorem fderivWithin_sum {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {x : E} {s : Set E} {ΞΉ : Type u_6} {u : Finset ΞΉ} {A : ΞΉ β E β F} (hxs : UniqueDiffWithinAt π s x) (h : β i β u, DifferentiableWithinAt π (A i) s x) :
fderivWithin π (fun (y : E) => u.sum fun (i : ΞΉ) => A i y) s x = u.sum fun (i : ΞΉ) => fderivWithin π (A i) s x
theorem fderiv_sum {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {x : E} {ΞΉ : Type u_6} {u : Finset ΞΉ} {A : ΞΉ β E β F} (h : β i β u, DifferentiableAt π (A i) x) :
fderiv π (fun (y : E) => u.sum fun (i : ΞΉ) => A i y) x = u.sum fun (i : ΞΉ) => fderiv π (A i) x

### Derivative of the negative of a function #

theorem HasStrictFDerivAt.neg {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {f' : E βL[π] F} {x : E} (h : ) :
HasStrictFDerivAt (fun (x : E) => -f x) (-f') x
theorem HasFDerivAtFilter.neg {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {f' : E βL[π] F} {x : E} {L : } (h : HasFDerivAtFilter f f' x L) :
HasFDerivAtFilter (fun (x : E) => -f x) (-f') x L
theorem HasFDerivWithinAt.neg {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} :
DifferentiableAt π (fun (y : E) => -f y) x β DifferentiableAt π f x
theorem DifferentiableOn.neg {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {s : Set E} :
DifferentiableOn π (fun (y : E) => -f y) s β DifferentiableOn π f s
theorem Differentiable.neg {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} (h : Differentiable π f) :
Differentiable π fun (y : E) => -f y
@[simp]
theorem differentiable_neg_iff {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} :
(Differentiable π fun (y : E) => -f y) β Differentiable π f
theorem fderivWithin_neg {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} {s : Set E} (hxs : UniqueDiffWithinAt π s x) :
fderivWithin π (fun (y : E) => -f y) s x = -fderivWithin π f s x
@[simp]
theorem fderiv_neg {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} :
fderiv π (fun (y : E) => -f y) x = -fderiv π f x

### Derivative of the difference of two functions #

theorem HasStrictFDerivAt.sub {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {g : E β F} {f' : E βL[π] F} {g' : E βL[π] F} {x : E} (hf : ) (hg : ) :
HasStrictFDerivAt (fun (x : E) => f x - g x) (f' - g') x
theorem HasFDerivAtFilter.sub {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {g : E β F} {f' : E βL[π] F} {g' : E βL[π] F} {x : E} {L : } (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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {g : E β F} {f' : E βL[π] F} {g' : E βL[π] F} {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) (hg : HasFDerivWithinAt g g' s x) :
HasFDerivWithinAt (fun (x : E) => f x - g x) (f' - g') s x
theorem HasFDerivAt.sub {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {g : E β F} {f' : E βL[π] F} {g' : E βL[π] F} {x : E} (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) :
HasFDerivAt (fun (x : E) => f x - g x) (f' - g') x
theorem DifferentiableWithinAt.sub {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {g : E β F} {x : E} {s : Set E} (hf : DifferentiableWithinAt π f s x) (hg : DifferentiableWithinAt π g s x) :
DifferentiableWithinAt π (fun (y : E) => f y - g y) s x
@[simp]
theorem DifferentiableAt.sub {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {g : E β F} {x : E} (hf : DifferentiableAt π f x) (hg : DifferentiableAt π g x) :
DifferentiableAt π (fun (y : E) => f y - g y) x
theorem DifferentiableOn.sub {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {g : E β F} {s : Set E} (hf : DifferentiableOn π f s) (hg : DifferentiableOn π g s) :
DifferentiableOn π (fun (y : E) => f y - g y) s
@[simp]
theorem Differentiable.sub {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {g : E β F} (hf : Differentiable π f) (hg : Differentiable π g) :
Differentiable π fun (y : E) => f y - g y
theorem fderivWithin_sub {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {g : E β F} {x : E} {s : Set E} (hxs : UniqueDiffWithinAt π s x) (hf : DifferentiableWithinAt π f s x) (hg : DifferentiableWithinAt π g s x) :
fderivWithin π (fun (y : E) => f y - g y) s x = fderivWithin π f s x - fderivWithin π g s x
theorem fderiv_sub {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {g : E β F} {x : E} (hf : DifferentiableAt π f x) (hg : DifferentiableAt π g x) :
fderiv π (fun (y : E) => f y - g y) x = fderiv π f x - fderiv π g x
theorem HasStrictFDerivAt.sub_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {f' : E βL[π] F} {x : E} (hf : ) (c : F) :
HasStrictFDerivAt (fun (x : E) => f x - c) f' x
theorem HasFDerivAtFilter.sub_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {f' : E βL[π] F} {x : E} {L : } (hf : HasFDerivAtFilter f f' x L) (c : F) :
HasFDerivAtFilter (fun (x : E) => f x - c) f' x L
theorem HasFDerivWithinAt.sub_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {f' : E βL[π] F} {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) (c : F) :
HasFDerivWithinAt (fun (x : E) => f x - c) f' s x
theorem HasFDerivAt.sub_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {f' : E βL[π] F} {x : E} (hf : HasFDerivAt f f' x) (c : F) :
HasFDerivAt (fun (x : E) => f x - c) f' x
theorem hasStrictFDerivAt_sub_const {π : Type u_1} [] {F : Type u_3} [NormedSpace π F] {x : F} (c : F) :
HasStrictFDerivAt (fun (x : F) => x - c) () x
theorem hasFDerivAt_sub_const {π : Type u_1} [] {F : Type u_3} [NormedSpace π F] {x : F} (c : F) :
HasFDerivAt (fun (x : F) => x - c) () x
theorem DifferentiableWithinAt.sub_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} (hf : DifferentiableAt π f x) (c : F) :
DifferentiableAt π (fun (y : E) => f y - c) x
@[simp]
theorem differentiableAt_sub_const_iff {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} (c : F) :
DifferentiableAt π (fun (y : E) => f y - c) x β DifferentiableAt π f x
theorem DifferentiableOn.sub_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {s : Set E} (hf : DifferentiableOn π f s) (c : F) :
DifferentiableOn π (fun (y : E) => f y - c) s
@[simp]
theorem differentiableOn_sub_const_iff {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {s : Set E} (c : F) :
DifferentiableOn π (fun (y : E) => f y - c) s β DifferentiableOn π f s
theorem Differentiable.sub_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} (hf : Differentiable π f) (c : F) :
Differentiable π fun (y : E) => f y - c
@[simp]
theorem differentiable_sub_const_iff {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} (c : F) :
(Differentiable π fun (y : E) => f y - c) β Differentiable π f
theorem fderivWithin_sub_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} {s : Set E} (hxs : UniqueDiffWithinAt π s x) (c : F) :
fderivWithin π (fun (y : E) => f y - c) s x = fderivWithin π f s x
theorem fderiv_sub_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} (c : F) :
fderiv π (fun (y : E) => f y - c) x = fderiv π f x
theorem HasStrictFDerivAt.const_sub {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {f' : E βL[π] F} {x : E} (hf : ) (c : F) :
HasStrictFDerivAt (fun (x : E) => c - f x) (-f') x
theorem HasFDerivAtFilter.const_sub {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {f' : E βL[π] F} {x : E} {L : } (hf : HasFDerivAtFilter f f' x L) (c : F) :
HasFDerivAtFilter (fun (x : E) => c - f x) (-f') x L
theorem HasFDerivWithinAt.const_sub {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} (hf : DifferentiableAt π f x) (c : F) :
DifferentiableAt π (fun (y : E) => c - f y) x
@[simp]
theorem differentiableAt_const_sub_iff {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} (c : F) :
DifferentiableAt π (fun (y : E) => c - f y) x β DifferentiableAt π f x
theorem DifferentiableOn.const_sub {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {s : Set E} (hf : DifferentiableOn π f s) (c : F) :
DifferentiableOn π (fun (y : E) => c - f y) s
@[simp]
theorem differentiableOn_const_sub_iff {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {s : Set E} (c : F) :
DifferentiableOn π (fun (y : E) => c - f y) s β DifferentiableOn π f s
theorem Differentiable.const_sub {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} (hf : Differentiable π f) (c : F) :
Differentiable π fun (y : E) => c - f y
@[simp]
theorem differentiable_const_sub_iff {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} (c : F) :
(Differentiable π fun (y : E) => c - f y) β Differentiable π f
theorem fderivWithin_const_sub {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} (c : F) :
fderiv π (fun (y : E) => c - f y) x = -fderiv π f x