One-dimensional derivatives of sums etc #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
has_deriv_at_filter.add
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f g : 𝕜 → F}
{f' g' : F}
{x : 𝕜}
{L : filter 𝕜}
(hf : has_deriv_at_filter f f' x L)
(hg : has_deriv_at_filter g g' x L) :
has_deriv_at_filter (λ (y : 𝕜), f y + g y) (f' + g') x L
theorem
has_strict_deriv_at.add
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f g : 𝕜 → F}
{f' g' : F}
{x : 𝕜}
(hf : has_strict_deriv_at f f' x)
(hg : has_strict_deriv_at g g' x) :
has_strict_deriv_at (λ (y : 𝕜), f y + g y) (f' + g') x
theorem
has_deriv_within_at.add
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f g : 𝕜 → F}
{f' g' : F}
{x : 𝕜}
{s : set 𝕜}
(hf : has_deriv_within_at f f' s x)
(hg : has_deriv_within_at g g' s x) :
has_deriv_within_at (λ (y : 𝕜), f y + g y) (f' + g') s x
theorem
has_deriv_at.add
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f g : 𝕜 → F}
{f' g' : F}
{x : 𝕜}
(hf : has_deriv_at f f' x)
(hg : has_deriv_at g g' x) :
has_deriv_at (λ (x : 𝕜), f x + g x) (f' + g') x
theorem
deriv_within_add
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f g : 𝕜 → F}
{x : 𝕜}
{s : set 𝕜}
(hxs : unique_diff_within_at 𝕜 s x)
(hf : differentiable_within_at 𝕜 f s x)
(hg : differentiable_within_at 𝕜 g s x) :
deriv_within (λ (y : 𝕜), f y + g y) s x = deriv_within f s x + deriv_within g s x
@[simp]
theorem
deriv_add
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f g : 𝕜 → F}
{x : 𝕜}
(hf : differentiable_at 𝕜 f x)
(hg : differentiable_at 𝕜 g x) :
theorem
has_deriv_at_filter.add_const
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{f' : F}
{x : 𝕜}
{L : filter 𝕜}
(hf : has_deriv_at_filter f f' x L)
(c : F) :
has_deriv_at_filter (λ (y : 𝕜), f y + c) f' x L
theorem
has_deriv_within_at.add_const
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{f' : F}
{x : 𝕜}
{s : set 𝕜}
(hf : has_deriv_within_at f f' s x)
(c : F) :
has_deriv_within_at (λ (y : 𝕜), f y + c) f' s x
theorem
has_deriv_at.add_const
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{f' : F}
{x : 𝕜}
(hf : has_deriv_at f f' x)
(c : F) :
has_deriv_at (λ (x : 𝕜), f x + c) f' x
theorem
deriv_within_add_const
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{x : 𝕜}
{s : set 𝕜}
(hxs : unique_diff_within_at 𝕜 s x)
(c : F) :
deriv_within (λ (y : 𝕜), f y + c) s x = deriv_within f s x
theorem
deriv_add_const
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{x : 𝕜}
(c : F) :
@[simp]
theorem
deriv_add_const'
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
(c : F) :
theorem
has_deriv_at_filter.const_add
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{f' : F}
{x : 𝕜}
{L : filter 𝕜}
(c : F)
(hf : has_deriv_at_filter f f' x L) :
has_deriv_at_filter (λ (y : 𝕜), c + f y) f' x L
theorem
has_deriv_within_at.const_add
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{f' : F}
{x : 𝕜}
{s : set 𝕜}
(c : F)
(hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (y : 𝕜), c + f y) f' s x
theorem
has_deriv_at.const_add
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{f' : F}
{x : 𝕜}
(c : F)
(hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : 𝕜), c + f x) f' x
theorem
deriv_within_const_add
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{x : 𝕜}
{s : set 𝕜}
(hxs : unique_diff_within_at 𝕜 s x)
(c : F) :
deriv_within (λ (y : 𝕜), c + f y) s x = deriv_within f s x
theorem
deriv_const_add
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{x : 𝕜}
(c : F) :
@[simp]
theorem
deriv_const_add'
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
(c : F) :
Derivative of a finite sum of functions #
theorem
has_deriv_at_filter.sum
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : 𝕜}
{L : filter 𝕜}
{ι : Type u_1}
{u : finset ι}
{A : ι → 𝕜 → F}
{A' : ι → F}
(h : ∀ (i : ι), i ∈ u → has_deriv_at_filter (A i) (A' i) x L) :
has_deriv_at_filter (λ (y : 𝕜), u.sum (λ (i : ι), A i y)) (u.sum (λ (i : ι), A' i)) x L
theorem
has_strict_deriv_at.sum
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : 𝕜}
{ι : Type u_1}
{u : finset ι}
{A : ι → 𝕜 → F}
{A' : ι → F}
(h : ∀ (i : ι), i ∈ u → has_strict_deriv_at (A i) (A' i) x) :
has_strict_deriv_at (λ (y : 𝕜), u.sum (λ (i : ι), A i y)) (u.sum (λ (i : ι), A' i)) x
theorem
has_deriv_within_at.sum
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : 𝕜}
{s : set 𝕜}
{ι : Type u_1}
{u : finset ι}
{A : ι → 𝕜 → F}
{A' : ι → F}
(h : ∀ (i : ι), i ∈ u → has_deriv_within_at (A i) (A' i) s x) :
has_deriv_within_at (λ (y : 𝕜), u.sum (λ (i : ι), A i y)) (u.sum (λ (i : ι), A' i)) s x
theorem
has_deriv_at.sum
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : 𝕜}
{ι : Type u_1}
{u : finset ι}
{A : ι → 𝕜 → F}
{A' : ι → F}
(h : ∀ (i : ι), i ∈ u → has_deriv_at (A i) (A' i) x) :
has_deriv_at (λ (y : 𝕜), u.sum (λ (i : ι), A i y)) (u.sum (λ (i : ι), A' i)) x
theorem
deriv_within_sum
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : 𝕜}
{s : set 𝕜}
{ι : Type u_1}
{u : finset ι}
{A : ι → 𝕜 → F}
(hxs : unique_diff_within_at 𝕜 s x)
(h : ∀ (i : ι), i ∈ u → differentiable_within_at 𝕜 (A i) s x) :
deriv_within (λ (y : 𝕜), u.sum (λ (i : ι), A i y)) s x = u.sum (λ (i : ι), deriv_within (A i) s x)
@[simp]
theorem
deriv_sum
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : 𝕜}
{ι : Type u_1}
{u : finset ι}
{A : ι → 𝕜 → F}
(h : ∀ (i : ι), i ∈ u → differentiable_at 𝕜 (A i) x) :
Derivative of the negative of a function #
theorem
has_deriv_at_filter.neg
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{f' : F}
{x : 𝕜}
{L : filter 𝕜}
(h : has_deriv_at_filter f f' x L) :
has_deriv_at_filter (λ (x : 𝕜), -f x) (-f') x L
theorem
has_deriv_within_at.neg
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{f' : F}
{x : 𝕜}
{s : set 𝕜}
(h : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : 𝕜), -f x) (-f') s x
theorem
has_deriv_at.neg
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{f' : F}
{x : 𝕜}
(h : has_deriv_at f f' x) :
has_deriv_at (λ (x : 𝕜), -f x) (-f') x
theorem
has_strict_deriv_at.neg
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{f' : F}
{x : 𝕜}
(h : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : 𝕜), -f x) (-f') x
theorem
deriv_within.neg
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{x : 𝕜}
{s : set 𝕜}
(hxs : unique_diff_within_at 𝕜 s x) :
deriv_within (λ (y : 𝕜), -f y) s x = -deriv_within f s x
theorem
deriv.neg
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{x : 𝕜} :
@[simp]
theorem
deriv.neg'
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F} :
Derivative of the negation function (i.e has_neg.neg) #
theorem
has_deriv_at_filter_neg
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
(x : 𝕜)
(L : filter 𝕜) :
has_deriv_at_filter has_neg.neg (-1) x L
theorem
has_deriv_within_at_neg
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
(x : 𝕜)
(s : set 𝕜) :
has_deriv_within_at has_neg.neg (-1) s x
theorem
has_deriv_at_neg
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
(x : 𝕜) :
has_deriv_at has_neg.neg (-1) x
theorem
has_deriv_at_neg'
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
(x : 𝕜) :
has_deriv_at (λ (x : 𝕜), -x) (-1) x
theorem
has_strict_deriv_at_neg
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
(x : 𝕜) :
has_strict_deriv_at has_neg.neg (-1) x
@[simp]
@[simp]
theorem
deriv_within_neg
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
(x : 𝕜)
(s : set 𝕜)
(hxs : unique_diff_within_at 𝕜 s x) :
deriv_within has_neg.neg s x = -1
Derivative of the difference of two functions #
theorem
has_deriv_at_filter.sub
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f g : 𝕜 → F}
{f' g' : F}
{x : 𝕜}
{L : filter 𝕜}
(hf : has_deriv_at_filter f f' x L)
(hg : has_deriv_at_filter g g' x L) :
has_deriv_at_filter (λ (x : 𝕜), f x - g x) (f' - g') x L
theorem
has_deriv_within_at.sub
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f g : 𝕜 → F}
{f' g' : F}
{x : 𝕜}
{s : set 𝕜}
(hf : has_deriv_within_at f f' s x)
(hg : has_deriv_within_at g g' s x) :
has_deriv_within_at (λ (x : 𝕜), f x - g x) (f' - g') s x
theorem
has_deriv_at.sub
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f g : 𝕜 → F}
{f' g' : F}
{x : 𝕜}
(hf : has_deriv_at f f' x)
(hg : has_deriv_at g g' x) :
has_deriv_at (λ (x : 𝕜), f x - g x) (f' - g') x
theorem
has_strict_deriv_at.sub
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f g : 𝕜 → F}
{f' g' : F}
{x : 𝕜}
(hf : has_strict_deriv_at f f' x)
(hg : has_strict_deriv_at g g' x) :
has_strict_deriv_at (λ (x : 𝕜), f x - g x) (f' - g') x
theorem
deriv_within_sub
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f g : 𝕜 → F}
{x : 𝕜}
{s : set 𝕜}
(hxs : unique_diff_within_at 𝕜 s x)
(hf : differentiable_within_at 𝕜 f s x)
(hg : differentiable_within_at 𝕜 g s x) :
deriv_within (λ (y : 𝕜), f y - g y) s x = deriv_within f s x - deriv_within g s x
@[simp]
theorem
deriv_sub
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f g : 𝕜 → F}
{x : 𝕜}
(hf : differentiable_at 𝕜 f x)
(hg : differentiable_at 𝕜 g x) :
theorem
has_deriv_at_filter.sub_const
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{f' : F}
{x : 𝕜}
{L : filter 𝕜}
(hf : has_deriv_at_filter f f' x L)
(c : F) :
has_deriv_at_filter (λ (x : 𝕜), f x - c) f' x L
theorem
has_deriv_within_at.sub_const
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{f' : F}
{x : 𝕜}
{s : set 𝕜}
(hf : has_deriv_within_at f f' s x)
(c : F) :
has_deriv_within_at (λ (x : 𝕜), f x - c) f' s x
theorem
has_deriv_at.sub_const
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{f' : F}
{x : 𝕜}
(hf : has_deriv_at f f' x)
(c : F) :
has_deriv_at (λ (x : 𝕜), f x - c) f' x
theorem
deriv_within_sub_const
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{x : 𝕜}
{s : set 𝕜}
(hxs : unique_diff_within_at 𝕜 s x)
(c : F) :
deriv_within (λ (y : 𝕜), f y - c) s x = deriv_within f s x
theorem
deriv_sub_const
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{x : 𝕜}
(c : F) :
theorem
has_deriv_at_filter.const_sub
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{f' : F}
{x : 𝕜}
{L : filter 𝕜}
(c : F)
(hf : has_deriv_at_filter f f' x L) :
has_deriv_at_filter (λ (x : 𝕜), c - f x) (-f') x L
theorem
has_deriv_within_at.const_sub
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{f' : F}
{x : 𝕜}
{s : set 𝕜}
(c : F)
(hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : 𝕜), c - f x) (-f') s x
theorem
has_strict_deriv_at.const_sub
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{f' : F}
{x : 𝕜}
(c : F)
(hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : 𝕜), c - f x) (-f') x
theorem
has_deriv_at.const_sub
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{f' : F}
{x : 𝕜}
(c : F)
(hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : 𝕜), c - f x) (-f') x
theorem
deriv_within_const_sub
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{x : 𝕜}
{s : set 𝕜}
(hxs : unique_diff_within_at 𝕜 s x)
(c : F) :
deriv_within (λ (y : 𝕜), c - f y) s x = -deriv_within f s x
theorem
deriv_const_sub
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{x : 𝕜}
(c : F) :