# One-dimensional derivatives of sums etc #

In this file we prove formulas about derivatives of f + g, -f, f - g, and ∑ i, f i x for functions from the base field to a normed space over this field.

For a more detailed overview of one-dimensional derivatives in mathlib, see the module docstring of Analysis/Calculus/Deriv/Basic.

## Keywords #

derivative

### Derivative of the sum of two functions #

theorem HasDerivAtFilter.add {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {g : 𝕜F} {f' : F} {g' : F} {x : 𝕜} {L : } (hf : HasDerivAtFilter f f' x L) (hg : HasDerivAtFilter g g' x L) :
HasDerivAtFilter (fun (y : 𝕜) => f y + g y) (f' + g') x L
theorem HasStrictDerivAt.add {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {g : 𝕜F} {f' : F} {g' : F} {x : 𝕜} (hf : HasStrictDerivAt f f' x) (hg : HasStrictDerivAt g g' x) :
HasStrictDerivAt (fun (y : 𝕜) => f y + g y) (f' + g') x
theorem HasDerivWithinAt.add {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {g : 𝕜F} {f' : F} {g' : F} {x : 𝕜} {s : Set 𝕜} (hf : HasDerivWithinAt f f' s x) (hg : HasDerivWithinAt g g' s x) :
HasDerivWithinAt (fun (y : 𝕜) => f y + g y) (f' + g') s x
theorem HasDerivAt.add {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {g : 𝕜F} {f' : F} {g' : F} {x : 𝕜} (hf : HasDerivAt f f' x) (hg : HasDerivAt g g' x) :
HasDerivAt (fun (x : 𝕜) => f x + g x) (f' + g') x
theorem derivWithin_add {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {g : 𝕜F} {x : 𝕜} {s : Set 𝕜} (hxs : ) (hf : ) (hg : ) :
derivWithin (fun (y : 𝕜) => f y + g y) s x = derivWithin f s x + derivWithin g s x
@[simp]
theorem deriv_add {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {g : 𝕜F} {x : 𝕜} (hf : ) (hg : ) :
deriv (fun (y : 𝕜) => f y + g y) x = deriv f x + deriv g x
theorem HasStrictDerivAt.add_const {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {f' : F} {x : 𝕜} (c : F) (hf : HasStrictDerivAt f f' x) :
HasStrictDerivAt (fun (y : 𝕜) => f y + c) f' x
theorem HasDerivAtFilter.add_const {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {f' : F} {x : 𝕜} {L : } (hf : HasDerivAtFilter f f' x L) (c : F) :
HasDerivAtFilter (fun (y : 𝕜) => f y + c) f' x L
theorem HasDerivWithinAt.add_const {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {f' : F} {x : 𝕜} {s : Set 𝕜} (hf : HasDerivWithinAt f f' s x) (c : F) :
HasDerivWithinAt (fun (y : 𝕜) => f y + c) f' s x
theorem HasDerivAt.add_const {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {f' : F} {x : 𝕜} (hf : HasDerivAt f f' x) (c : F) :
HasDerivAt (fun (x : 𝕜) => f x + c) f' x
theorem derivWithin_add_const {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {x : 𝕜} {s : Set 𝕜} (hxs : ) (c : F) :
derivWithin (fun (y : 𝕜) => f y + c) s x = derivWithin f s x
theorem deriv_add_const {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {x : 𝕜} (c : F) :
deriv (fun (y : 𝕜) => f y + c) x = deriv f x
@[simp]
theorem deriv_add_const' {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} (c : F) :
(deriv fun (y : 𝕜) => f y + c) =
theorem HasStrictDerivAt.const_add {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {f' : F} {x : 𝕜} (c : F) (hf : HasStrictDerivAt f f' x) :
HasStrictDerivAt (fun (y : 𝕜) => c + f y) f' x
theorem HasDerivAtFilter.const_add {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {f' : F} {x : 𝕜} {L : } (c : F) (hf : HasDerivAtFilter f f' x L) :
HasDerivAtFilter (fun (y : 𝕜) => c + f y) f' x L
theorem HasDerivWithinAt.const_add {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {f' : F} {x : 𝕜} {s : Set 𝕜} (c : F) (hf : HasDerivWithinAt f f' s x) :
HasDerivWithinAt (fun (y : 𝕜) => c + f y) f' s x
theorem HasDerivAt.const_add {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {f' : F} {x : 𝕜} (c : F) (hf : HasDerivAt f f' x) :
HasDerivAt (fun (x : 𝕜) => c + f x) f' x
theorem derivWithin_const_add {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {x : 𝕜} {s : Set 𝕜} (hxs : ) (c : F) :
derivWithin (fun (y : 𝕜) => c + f y) s x = derivWithin f s x
theorem deriv_const_add {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {x : 𝕜} (c : F) :
deriv (fun (y : 𝕜) => c + f y) x = deriv f x
@[simp]
theorem deriv_const_add' {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} (c : F) :
(deriv fun (y : 𝕜) => c + f y) =
theorem differentiableAt_comp_const_add {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {a : 𝕜} {b : 𝕜} :
DifferentiableAt 𝕜 (fun (x : 𝕜) => f (b + x)) a DifferentiableAt 𝕜 f (b + a)
theorem differentiableAt_comp_add_const {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {a : 𝕜} {b : 𝕜} :
DifferentiableAt 𝕜 (fun (x : 𝕜) => f (x + b)) a DifferentiableAt 𝕜 f (a + b)
theorem differentiableAt_iff_comp_const_add {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {a : 𝕜} {b : 𝕜} :
DifferentiableAt 𝕜 (fun (x : 𝕜) => f (b + x)) (-b + a)
theorem differentiableAt_iff_comp_add_const {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {a : 𝕜} {b : 𝕜} :
DifferentiableAt 𝕜 (fun (x : 𝕜) => f (x + b)) (a - b)

### Derivative of a finite sum of functions #

theorem HasDerivAtFilter.sum {𝕜 : Type u} {F : Type v} [] {x : 𝕜} {L : } {ι : Type u_1} {u : } {A : ι𝕜F} {A' : ιF} (h : iu, HasDerivAtFilter (A i) (A' i) x L) :
HasDerivAtFilter (fun (y : 𝕜) => iu, A i y) (∑ iu, A' i) x L
theorem HasStrictDerivAt.sum {𝕜 : Type u} {F : Type v} [] {x : 𝕜} {ι : Type u_1} {u : } {A : ι𝕜F} {A' : ιF} (h : iu, HasStrictDerivAt (A i) (A' i) x) :
HasStrictDerivAt (fun (y : 𝕜) => iu, A i y) (∑ iu, A' i) x
theorem HasDerivWithinAt.sum {𝕜 : Type u} {F : Type v} [] {x : 𝕜} {s : Set 𝕜} {ι : Type u_1} {u : } {A : ι𝕜F} {A' : ιF} (h : iu, HasDerivWithinAt (A i) (A' i) s x) :
HasDerivWithinAt (fun (y : 𝕜) => iu, A i y) (∑ iu, A' i) s x
theorem HasDerivAt.sum {𝕜 : Type u} {F : Type v} [] {x : 𝕜} {ι : Type u_1} {u : } {A : ι𝕜F} {A' : ιF} (h : iu, HasDerivAt (A i) (A' i) x) :
HasDerivAt (fun (y : 𝕜) => iu, A i y) (∑ iu, A' i) x
theorem derivWithin_sum {𝕜 : Type u} {F : Type v} [] {x : 𝕜} {s : Set 𝕜} {ι : Type u_1} {u : } {A : ι𝕜F} (hxs : ) (h : iu, DifferentiableWithinAt 𝕜 (A i) s x) :
derivWithin (fun (y : 𝕜) => iu, A i y) s x = iu, derivWithin (A i) s x
@[simp]
theorem deriv_sum {𝕜 : Type u} {F : Type v} [] {x : 𝕜} {ι : Type u_1} {u : } {A : ι𝕜F} (h : iu, DifferentiableAt 𝕜 (A i) x) :
deriv (fun (y : 𝕜) => iu, A i y) x = iu, deriv (A i) x

### Derivative of the negative of a function #

theorem HasDerivAtFilter.neg {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {f' : F} {x : 𝕜} {L : } (h : HasDerivAtFilter f f' x L) :
HasDerivAtFilter (fun (x : 𝕜) => -f x) (-f') x L
theorem HasDerivWithinAt.neg {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {f' : F} {x : 𝕜} {s : Set 𝕜} (h : HasDerivWithinAt f f' s x) :
HasDerivWithinAt (fun (x : 𝕜) => -f x) (-f') s x
theorem HasDerivAt.neg {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {f' : F} {x : 𝕜} (h : HasDerivAt f f' x) :
HasDerivAt (fun (x : 𝕜) => -f x) (-f') x
theorem HasStrictDerivAt.neg {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {f' : F} {x : 𝕜} (h : HasStrictDerivAt f f' x) :
HasStrictDerivAt (fun (x : 𝕜) => -f x) (-f') x
theorem derivWithin.neg {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {x : 𝕜} {s : Set 𝕜} (hxs : ) :
derivWithin (fun (y : 𝕜) => -f y) s x = -derivWithin f s x
theorem deriv.neg {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {x : 𝕜} :
deriv (fun (y : 𝕜) => -f y) x = -deriv f x
@[simp]
theorem deriv.neg' {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} :
(deriv fun (y : 𝕜) => -f y) = fun (x : 𝕜) => -deriv f x

### Derivative of the negation function (i.e Neg.neg) #

theorem hasDerivAtFilter_neg {𝕜 : Type u} (x : 𝕜) (L : ) :
HasDerivAtFilter Neg.neg (-1) x L
theorem hasDerivWithinAt_neg {𝕜 : Type u} (x : 𝕜) (s : Set 𝕜) :
HasDerivWithinAt Neg.neg (-1) s x
theorem hasDerivAt_neg {𝕜 : Type u} (x : 𝕜) :
HasDerivAt Neg.neg (-1) x
theorem hasDerivAt_neg' {𝕜 : Type u} (x : 𝕜) :
HasDerivAt (fun (x : 𝕜) => -x) (-1) x
theorem hasStrictDerivAt_neg {𝕜 : Type u} (x : 𝕜) :
HasStrictDerivAt Neg.neg (-1) x
theorem deriv_neg {𝕜 : Type u} (x : 𝕜) :
deriv Neg.neg x = -1
@[simp]
theorem deriv_neg' {𝕜 : Type u} :
deriv Neg.neg = fun (x : 𝕜) => -1
@[simp]
theorem deriv_neg'' {𝕜 : Type u} (x : 𝕜) :
deriv (fun (x : 𝕜) => -x) x = -1
theorem derivWithin_neg {𝕜 : Type u} (x : 𝕜) (s : Set 𝕜) (hxs : ) :
derivWithin Neg.neg s x = -1
theorem differentiable_neg {𝕜 : Type u} :
Differentiable 𝕜 Neg.neg
theorem differentiableOn_neg {𝕜 : Type u} (s : Set 𝕜) :
DifferentiableOn 𝕜 Neg.neg s
theorem differentiableAt_comp_neg {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {a : 𝕜} :
DifferentiableAt 𝕜 (fun (x : 𝕜) => f (-x)) a DifferentiableAt 𝕜 f (-a)
theorem differentiableAt_iff_comp_neg {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {a : 𝕜} :
DifferentiableAt 𝕜 (fun (x : 𝕜) => f (-x)) (-a)

### Derivative of the difference of two functions #

theorem HasDerivAtFilter.sub {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {g : 𝕜F} {f' : F} {g' : F} {x : 𝕜} {L : } (hf : HasDerivAtFilter f f' x L) (hg : HasDerivAtFilter g g' x L) :
HasDerivAtFilter (fun (x : 𝕜) => f x - g x) (f' - g') x L
theorem HasDerivWithinAt.sub {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {g : 𝕜F} {f' : F} {g' : F} {x : 𝕜} {s : Set 𝕜} (hf : HasDerivWithinAt f f' s x) (hg : HasDerivWithinAt g g' s x) :
HasDerivWithinAt (fun (x : 𝕜) => f x - g x) (f' - g') s x
theorem HasDerivAt.sub {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {g : 𝕜F} {f' : F} {g' : F} {x : 𝕜} (hf : HasDerivAt f f' x) (hg : HasDerivAt g g' x) :
HasDerivAt (fun (x : 𝕜) => f x - g x) (f' - g') x
theorem HasStrictDerivAt.sub {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {g : 𝕜F} {f' : F} {g' : F} {x : 𝕜} (hf : HasStrictDerivAt f f' x) (hg : HasStrictDerivAt g g' x) :
HasStrictDerivAt (fun (x : 𝕜) => f x - g x) (f' - g') x
theorem derivWithin_sub {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {g : 𝕜F} {x : 𝕜} {s : Set 𝕜} (hxs : ) (hf : ) (hg : ) :
derivWithin (fun (y : 𝕜) => f y - g y) s x = derivWithin f s x - derivWithin g s x
@[simp]
theorem deriv_sub {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {g : 𝕜F} {x : 𝕜} (hf : ) (hg : ) :
deriv (fun (y : 𝕜) => f y - g y) x = deriv f x - deriv g x
theorem HasDerivAtFilter.sub_const {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {f' : F} {x : 𝕜} {L : } (hf : HasDerivAtFilter f f' x L) (c : F) :
HasDerivAtFilter (fun (x : 𝕜) => f x - c) f' x L
theorem HasDerivWithinAt.sub_const {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {f' : F} {x : 𝕜} {s : Set 𝕜} (hf : HasDerivWithinAt f f' s x) (c : F) :
HasDerivWithinAt (fun (x : 𝕜) => f x - c) f' s x
theorem HasDerivAt.sub_const {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {f' : F} {x : 𝕜} (hf : HasDerivAt f f' x) (c : F) :
HasDerivAt (fun (x : 𝕜) => f x - c) f' x
theorem derivWithin_sub_const {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {x : 𝕜} {s : Set 𝕜} (hxs : ) (c : F) :
derivWithin (fun (y : 𝕜) => f y - c) s x = derivWithin f s x
theorem deriv_sub_const {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {x : 𝕜} (c : F) :
deriv (fun (y : 𝕜) => f y - c) x = deriv f x
theorem HasDerivAtFilter.const_sub {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {f' : F} {x : 𝕜} {L : } (c : F) (hf : HasDerivAtFilter f f' x L) :
HasDerivAtFilter (fun (x : 𝕜) => c - f x) (-f') x L
theorem HasDerivWithinAt.const_sub {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {f' : F} {x : 𝕜} {s : Set 𝕜} (c : F) (hf : HasDerivWithinAt f f' s x) :
HasDerivWithinAt (fun (x : 𝕜) => c - f x) (-f') s x
theorem HasStrictDerivAt.const_sub {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {f' : F} {x : 𝕜} (c : F) (hf : HasStrictDerivAt f f' x) :
HasStrictDerivAt (fun (x : 𝕜) => c - f x) (-f') x
theorem HasDerivAt.const_sub {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {f' : F} {x : 𝕜} (c : F) (hf : HasDerivAt f f' x) :
HasDerivAt (fun (x : 𝕜) => c - f x) (-f') x
theorem derivWithin_const_sub {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {x : 𝕜} {s : Set 𝕜} (hxs : ) (c : F) :
derivWithin (fun (y : 𝕜) => c - f y) s x = -derivWithin f s x
theorem deriv_const_sub {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {x : 𝕜} (c : F) :
deriv (fun (y : 𝕜) => c - f y) x = -deriv f x
theorem differentiableAt_comp_sub_const {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {a : 𝕜} {b : 𝕜} :
DifferentiableAt 𝕜 (fun (x : 𝕜) => f (x - b)) a DifferentiableAt 𝕜 f (a - b)
theorem differentiableAt_comp_const_sub {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {a : 𝕜} {b : 𝕜} :
DifferentiableAt 𝕜 (fun (x : 𝕜) => f (b - x)) a DifferentiableAt 𝕜 f (b - a)
theorem differentiableAt_iff_comp_sub_const {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {a : 𝕜} {b : 𝕜} :
DifferentiableAt 𝕜 (fun (x : 𝕜) => f (x - b)) (a + b)
theorem differentiableAt_iff_comp_const_sub {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {a : 𝕜} {b : 𝕜} :
DifferentiableAt 𝕜 (fun (x : 𝕜) => f (b - x)) (b - a)