Documentation

Mathlib.Analysis.Calculus.Deriv.Add

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} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {g : 𝕜F} {f' : F} {g' : F} {x : 𝕜} {L : Filter 𝕜} (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} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {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} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {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} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {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} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {g : 𝕜F} {x : 𝕜} {s : Set 𝕜} (hxs : UniqueDiffWithinAt 𝕜 s x) (hf : DifferentiableWithinAt 𝕜 f s x) (hg : DifferentiableWithinAt 𝕜 g s x) :
derivWithin (fun (y : 𝕜) => f y + g y) s x = derivWithin f s x + derivWithin g s x
@[simp]
theorem deriv_add {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {g : 𝕜F} {x : 𝕜} (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :
deriv (fun (y : 𝕜) => f y + g y) x = deriv f x + deriv g x
theorem HasStrictDerivAt.add_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {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} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {f' : F} {x : 𝕜} {L : Filter 𝕜} (hf : HasDerivAtFilter f f' x L) (c : F) :
HasDerivAtFilter (fun (y : 𝕜) => f y + c) f' x L
theorem HasDerivWithinAt.add_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {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} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {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} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {x : 𝕜} {s : Set 𝕜} (hxs : UniqueDiffWithinAt 𝕜 s x) (c : F) :
derivWithin (fun (y : 𝕜) => f y + c) s x = derivWithin f s x
theorem deriv_add_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {x : 𝕜} (c : F) :
deriv (fun (y : 𝕜) => f y + c) x = deriv f x
@[simp]
theorem deriv_add_const' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} (c : F) :
(deriv fun (y : 𝕜) => f y + c) = deriv f
theorem HasStrictDerivAt.const_add {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {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} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {f' : F} {x : 𝕜} {L : Filter 𝕜} (c : F) (hf : HasDerivAtFilter f f' x L) :
HasDerivAtFilter (fun (y : 𝕜) => c + f y) f' x L
theorem HasDerivWithinAt.const_add {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {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} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {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} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {x : 𝕜} {s : Set 𝕜} (hxs : UniqueDiffWithinAt 𝕜 s x) (c : F) :
derivWithin (fun (y : 𝕜) => c + f y) s x = derivWithin f s x
theorem deriv_const_add {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {x : 𝕜} (c : F) :
deriv (fun (y : 𝕜) => c + f y) x = deriv f x
@[simp]
theorem deriv_const_add' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} (c : F) :
(deriv fun (y : 𝕜) => c + f y) = deriv f

Derivative of a finite sum of functions #

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

Derivative of the negative of a function #

theorem HasDerivAtFilter.neg {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {f' : F} {x : 𝕜} {L : Filter 𝕜} (h : HasDerivAtFilter f f' x L) :
HasDerivAtFilter (fun (x : 𝕜) => -f x) (-f') x L
theorem HasDerivWithinAt.neg {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {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} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {f' : F} {x : 𝕜} (h : HasDerivAt f f' x) :
HasDerivAt (fun (x : 𝕜) => -f x) (-f') x
theorem HasStrictDerivAt.neg {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {f' : F} {x : 𝕜} (h : HasStrictDerivAt f f' x) :
HasStrictDerivAt (fun (x : 𝕜) => -f x) (-f') x
theorem derivWithin.neg {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {x : 𝕜} {s : Set 𝕜} (hxs : UniqueDiffWithinAt 𝕜 s x) :
derivWithin (fun (y : 𝕜) => -f y) s x = -derivWithin f s x
theorem deriv.neg {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {x : 𝕜} :
deriv (fun (y : 𝕜) => -f y) x = -deriv f x
@[simp]
theorem deriv.neg' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {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} [NontriviallyNormedField 𝕜] (x : 𝕜) (L : Filter 𝕜) :
HasDerivAtFilter Neg.neg (-1) x L
theorem hasDerivWithinAt_neg {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) (s : Set 𝕜) :
HasDerivWithinAt Neg.neg (-1) s x
theorem hasDerivAt_neg {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) :
HasDerivAt Neg.neg (-1) x
theorem hasDerivAt_neg' {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) :
HasDerivAt (fun (x : 𝕜) => -x) (-1) x
theorem hasStrictDerivAt_neg {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) :
HasStrictDerivAt Neg.neg (-1) x
theorem deriv_neg {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) :
deriv Neg.neg x = -1
@[simp]
theorem deriv_neg' {𝕜 : Type u} [NontriviallyNormedField 𝕜] :
deriv Neg.neg = fun (x : 𝕜) => -1
@[simp]
theorem deriv_neg'' {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) :
deriv (fun (x : 𝕜) => -x) x = -1
theorem derivWithin_neg {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) (s : Set 𝕜) (hxs : UniqueDiffWithinAt 𝕜 s x) :
derivWithin Neg.neg s x = -1
theorem differentiableOn_neg {𝕜 : Type u} [NontriviallyNormedField 𝕜] (s : Set 𝕜) :
DifferentiableOn 𝕜 Neg.neg s
theorem differentiableAt_comp_neg_iff {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {a : 𝕜} :
DifferentiableAt 𝕜 f (-a) DifferentiableAt 𝕜 (fun (x : 𝕜) => f (-x)) a

Derivative of the difference of two functions #

theorem HasDerivAtFilter.sub {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {g : 𝕜F} {f' : F} {g' : F} {x : 𝕜} {L : Filter 𝕜} (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} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {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} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {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} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {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} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {g : 𝕜F} {x : 𝕜} {s : Set 𝕜} (hxs : UniqueDiffWithinAt 𝕜 s x) (hf : DifferentiableWithinAt 𝕜 f s x) (hg : DifferentiableWithinAt 𝕜 g s x) :
derivWithin (fun (y : 𝕜) => f y - g y) s x = derivWithin f s x - derivWithin g s x
@[simp]
theorem deriv_sub {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {g : 𝕜F} {x : 𝕜} (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :
deriv (fun (y : 𝕜) => f y - g y) x = deriv f x - deriv g x
theorem HasDerivAtFilter.sub_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {f' : F} {x : 𝕜} {L : Filter 𝕜} (hf : HasDerivAtFilter f f' x L) (c : F) :
HasDerivAtFilter (fun (x : 𝕜) => f x - c) f' x L
theorem HasDerivWithinAt.sub_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {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} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {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} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {x : 𝕜} {s : Set 𝕜} (hxs : UniqueDiffWithinAt 𝕜 s x) (c : F) :
derivWithin (fun (y : 𝕜) => f y - c) s x = derivWithin f s x
theorem deriv_sub_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {x : 𝕜} (c : F) :
deriv (fun (y : 𝕜) => f y - c) x = deriv f x
theorem HasDerivAtFilter.const_sub {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {f' : F} {x : 𝕜} {L : Filter 𝕜} (c : F) (hf : HasDerivAtFilter f f' x L) :
HasDerivAtFilter (fun (x : 𝕜) => c - f x) (-f') x L
theorem HasDerivWithinAt.const_sub {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {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} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {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} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {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} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {x : 𝕜} {s : Set 𝕜} (hxs : UniqueDiffWithinAt 𝕜 s x) (c : F) :
derivWithin (fun (y : 𝕜) => c - f y) s x = -derivWithin f s x
theorem deriv_const_sub {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {x : 𝕜} (c : F) :
deriv (fun (y : 𝕜) => c - f y) x = -deriv f x