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)
:
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)
:
@[simp]
theorem
deriv_add_const'
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : 𝕜 → F}
(c : 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)
:
@[simp]
theorem
deriv_const_add'
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : 𝕜 → F}
(c : 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 : ∀ i ∈ u, HasDerivAtFilter (A i) (A' i) x L)
:
HasDerivAtFilter (fun (y : 𝕜) => ∑ i ∈ u, A i y) (∑ i ∈ u, 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 : ∀ i ∈ u, HasStrictDerivAt (A i) (A' i) x)
:
HasStrictDerivAt (fun (y : 𝕜) => ∑ i ∈ u, A i y) (∑ i ∈ u, 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 : ∀ i ∈ u, HasDerivWithinAt (A i) (A' i) s x)
:
HasDerivWithinAt (fun (y : 𝕜) => ∑ i ∈ u, A i y) (∑ i ∈ u, 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 : ∀ i ∈ u, HasDerivAt (A i) (A' i) x)
:
HasDerivAt (fun (y : 𝕜) => ∑ i ∈ u, A i y) (∑ i ∈ u, 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 : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x)
:
derivWithin (fun (y : 𝕜) => ∑ i ∈ u, A i y) s x = ∑ i ∈ u, 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 : ∀ i ∈ u, DifferentiableAt 𝕜 (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 : 𝕜}
:
@[simp]
theorem
deriv.neg'
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : 𝕜 → F}
:
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 (fun (x : 𝕜) => -x) (-1) x
theorem
hasStrictDerivAt_neg
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
(x : 𝕜)
:
HasStrictDerivAt Neg.neg (-1) x
@[simp]
@[simp]
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)
:
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)
:
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)
: