One-dimensional derivatives
This file defines the derivative of a function f : π β F where π is a
normed field and F is a normed space over this field. The derivative of
such a function f at a point x is given by an element f' : F.
The theory is developed analogously to the FrΓ©chet derivatives. We first introduce predicates defined in terms of the corresponding predicates for FrΓ©chet derivatives:
has_deriv_at_filter f f' x Lstates that the functionfhas the derivativef'at the pointxasxgoes along the filterL.has_deriv_within_at f f' s xstates that the functionfhas the derivativef'at the pointxwithin the subsets.has_deriv_at f f' xstates that the functionfhas the derivativef'at the pointx.has_strict_deriv_at f f' xstates that the functionfhas the derivativef'at the pointxin the sense of strict differentiability, i.e.,f y - f z = (y - z) β’ f' + o (y - z)asy, z β x.
For the last two notions we also define a functional version:
deriv_within f s xis a derivative offatxwithins. If the derivative does not exist, thenderiv_within f s xequals zero.deriv f xis a derivative offatx. If the derivative does not exist, thenderiv f xequals zero.
The theorems fderiv_within_deriv_within and fderiv_deriv show that the
one-dimensional derivatives coincide with the general FrΓ©chet derivatives.
We also show the existence and compute the derivatives of:
- constants
- the identity function
- linear maps
- addition
- sum of finitely many functions
- negation
- subtraction
- multiplication
- inverse
x β xβ»ΒΉ - multiplication of two functions in
π β π - multiplication of a function in
π β πand of a function inπ β E - composition of a function in
π β Fwith a function inπ β π - composition of a function in
F β Ewith a function inπ β F - inverse function (assuming that it exists; the inverse function theorem is in
inverse.lean) - division
- polynomials
For most binary operations we also define const_op and op_const theorems for the cases when
the first or second argument is a constant. This makes writing chains of has_deriv_at's easier,
and they more frequently lead to the desired result.
We set up the simplifier so that it can compute the derivative of simple functions. For instance,
example (x : β) : deriv (Ξ» x, cos (sin x) * exp x) x = (cos(sin(x))-sin(sin(x))*cos(x))*exp(x) :=
by { simp, ring }
Implementation notes
Most of the theorems are direct restatements of the corresponding theorems for FrΓ©chet derivatives.
The strategy to construct simp lemmas that give the simplifier the possibility to compute
derivatives is the same as the one for differentiability statements, as explained in fderiv.lean.
See the explanations there.
def
has_deriv_at_filter
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F] :
(π β F) β F β π β filter π β Prop
f has the derivative f' at the point x as x goes along the filter L.
That is, f x' = f x + (x' - x) β’ f' + o(x' - x) where x' converges along the filter L.
Equations
- has_deriv_at_filter f f' x L = has_fderiv_at_filter f (1.smul_right f') x L
def
has_deriv_within_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F] :
(π β F) β F β set π β π β Prop
f has the derivative f' at the point x within the subset s.
That is, f x' = f x + (x' - x) β’ f' + o(x' - x) where x' converges to x inside s.
Equations
- has_deriv_within_at f f' s x = has_deriv_at_filter f f' x (nhds_within x s)
def
has_deriv_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F] :
(π β F) β F β π β Prop
f has the derivative f' at the point x.
That is, f x' = f x + (x' - x) β’ f' + o(x' - x) where x' converges to x.
Equations
- has_deriv_at f f' x = has_deriv_at_filter f f' x (nhds x)
def
has_strict_deriv_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F] :
(π β F) β F β π β Prop
f has the derivative f' at the point x in the sense of strict differentiability.
That is, f y - f z = (y - z) β’ f' + o(y - z) as y, z β x.
Equations
- has_strict_deriv_at f f' x = has_strict_fderiv_at f (1.smul_right f') x
def
deriv_within
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F] :
(π β F) β set π β π β F
Derivative of f at the point x within the set s, if it exists. Zero otherwise.
If the derivative exists (i.e., β f', has_deriv_within_at f f' s x), then
f x' = f x + (x' - x) β’ deriv_within f s x + o(x' - x) where x' converges to x inside s.
Equations
- deriv_within f s x = β(fderiv_within π f s x) 1
def
deriv
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F] :
(π β F) β π β F
Derivative of f at the point x, if it exists. Zero otherwise.
If the derivative exists (i.e., β f', has_deriv_at f f' x), then
f x' = f x + (x' - x) β’ deriv f x + o(x' - x) where x' converges to x.
theorem
has_fderiv_at_filter_iff_has_deriv_at_filter
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
{L : filter π}
{f' : π βL[π] F} :
has_fderiv_at_filter f f' x L β has_deriv_at_filter f (βf' 1) x L
Expressing has_fderiv_at_filter f f' x L in terms of has_deriv_at_filter
theorem
has_fderiv_at_filter.has_deriv_at_filter
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
{L : filter π}
{f' : π βL[π] F} :
has_fderiv_at_filter f f' x L β has_deriv_at_filter f (βf' 1) x L
theorem
has_fderiv_within_at_iff_has_deriv_within_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s : set π}
{f' : π βL[π] F} :
has_fderiv_within_at f f' s x β has_deriv_within_at f (βf' 1) s x
Expressing has_fderiv_within_at f f' s x in terms of has_deriv_within_at
theorem
has_deriv_within_at_iff_has_fderiv_within_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s : set π}
{f' : F} :
has_deriv_within_at f f' s x β has_fderiv_within_at f (1.smul_right f') s x
Expressing has_deriv_within_at f f' s x in terms of has_fderiv_within_at
theorem
has_fderiv_within_at.has_deriv_within_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s : set π}
{f' : π βL[π] F} :
has_fderiv_within_at f f' s x β has_deriv_within_at f (βf' 1) s x
theorem
has_deriv_within_at.has_fderiv_within_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s : set π}
{f' : F} :
has_deriv_within_at f f' s x β has_fderiv_within_at f (1.smul_right f') s x
theorem
has_fderiv_at_iff_has_deriv_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
{f' : π βL[π] F} :
has_fderiv_at f f' x β has_deriv_at f (βf' 1) x
Expressing has_fderiv_at f f' x in terms of has_deriv_at
theorem
has_fderiv_at.has_deriv_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
{f' : π βL[π] F} :
has_fderiv_at f f' x β has_deriv_at f (βf' 1) x
theorem
has_strict_fderiv_at_iff_has_strict_deriv_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
{f' : π βL[π] F} :
has_strict_fderiv_at f f' x β has_strict_deriv_at f (βf' 1) x
theorem
has_strict_fderiv_at.has_strict_deriv_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
{f' : π βL[π] F} :
has_strict_fderiv_at f f' x β has_strict_deriv_at f (βf' 1) x
theorem
has_deriv_at_iff_has_fderiv_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
{f' : F} :
has_deriv_at f f' x β has_fderiv_at f (1.smul_right f') x
Expressing has_deriv_at f f' x in terms of has_fderiv_at
theorem
deriv_within_zero_of_not_differentiable_within_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s : set π} :
Β¬differentiable_within_at π f s x β deriv_within f s x = 0
theorem
deriv_zero_of_not_differentiable_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π} :
Β¬differentiable_at π f x β deriv f x = 0
theorem
unique_diff_within_at.eq_deriv
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' fβ' : F}
{x : π}
(s : set π) :
unique_diff_within_at π s x β has_deriv_within_at f f' s x β has_deriv_within_at f fβ' s x β f' = fβ'
theorem
has_deriv_at_filter_iff_tendsto
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{L : filter π} :
theorem
has_deriv_within_at_iff_tendsto
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s : set π} :
theorem
has_deriv_at_iff_tendsto
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π} :
theorem
has_strict_deriv_at.has_deriv_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π} :
has_strict_deriv_at f f' x β has_deriv_at f f' x
theorem
has_deriv_at_filter_iff_tendsto_slope
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{L : filter π} :
has_deriv_at_filter f f' x L β filter.tendsto (Ξ» (y : π), (y - x)β»ΒΉ β’ (f y - f x)) (L β filter.principal {x}αΆ) (nhds f')
If the domain has dimension one, then FrΓ©chet derivative is equivalent to the classical
definition with a limit. In this version we have to take the limit along the subset -{x},
because for y=x the slope equals zero due to the convention 0β»ΒΉ=0.
theorem
has_deriv_within_at_iff_tendsto_slope
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s : set π} :
has_deriv_within_at f f' s x β filter.tendsto (Ξ» (y : π), (y - x)β»ΒΉ β’ (f y - f x)) (nhds_within x (s \ {x})) (nhds f')
theorem
has_deriv_within_at_iff_tendsto_slope'
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s : set π} :
x β s β (has_deriv_within_at f f' s x β filter.tendsto (Ξ» (y : π), (y - x)β»ΒΉ β’ (f y - f x)) (nhds_within x s) (nhds f'))
theorem
has_deriv_at_iff_tendsto_slope
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π} :
has_deriv_at f f' x β filter.tendsto (Ξ» (y : π), (y - x)β»ΒΉ β’ (f y - f x)) (nhds_within x {x}αΆ) (nhds f')
theorem
has_deriv_at_iff_is_o_nhds_zero
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π} :
has_deriv_at f f' x β asymptotics.is_o (Ξ» (h : π), f (x + h) - f x - h β’ f') (Ξ» (h : π), h) (nhds 0)
theorem
has_deriv_at_filter.mono
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{Lβ Lβ : filter π} :
has_deriv_at_filter f f' x Lβ β Lβ β€ Lβ β has_deriv_at_filter f f' x Lβ
theorem
has_deriv_within_at.mono
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s t : set π} :
has_deriv_within_at f f' t x β s β t β has_deriv_within_at f f' s x
theorem
has_deriv_at.has_deriv_at_filter
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{L : filter π} :
has_deriv_at f f' x β L β€ nhds x β has_deriv_at_filter f f' x L
theorem
has_deriv_at.has_deriv_within_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s : set π} :
has_deriv_at f f' x β has_deriv_within_at f f' s x
theorem
has_deriv_within_at.differentiable_within_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s : set π} :
has_deriv_within_at f f' s x β differentiable_within_at π f s x
theorem
has_deriv_at.differentiable_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π} :
has_deriv_at f f' x β differentiable_at π f x
@[simp]
theorem
has_deriv_within_at_univ
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π} :
has_deriv_within_at f f' set.univ x β has_deriv_at f f' x
theorem
has_deriv_at_unique
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{fβ' fβ' : F}
{x : π} :
has_deriv_at f fβ' x β has_deriv_at f fβ' x β fβ' = fβ'
theorem
has_deriv_within_at_inter'
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s t : set π} :
t β nhds_within x s β (has_deriv_within_at f f' (s β© t) x β has_deriv_within_at f f' s x)
theorem
has_deriv_within_at_inter
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s t : set π} :
t β nhds x β (has_deriv_within_at f f' (s β© t) x β has_deriv_within_at f f' s x)
theorem
has_deriv_within_at.union
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s t : set π} :
has_deriv_within_at f f' s x β has_deriv_within_at f f' t x β has_deriv_within_at f f' (s βͺ t) x
theorem
has_deriv_within_at.nhds_within
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s t : set π} :
has_deriv_within_at f f' s x β s β nhds_within x t β has_deriv_within_at f f' t x
theorem
has_deriv_within_at.has_deriv_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s : set π} :
has_deriv_within_at f f' s x β s β nhds x β has_deriv_at f f' x
theorem
differentiable_within_at.has_deriv_within_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s : set π} :
differentiable_within_at π f s x β has_deriv_within_at f (deriv_within f s x) s x
theorem
differentiable_at.has_deriv_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π} :
differentiable_at π f x β has_deriv_at f (deriv f x) x
theorem
has_deriv_at.deriv
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π} :
has_deriv_at f f' x β deriv f x = f'
theorem
has_deriv_within_at.deriv_within
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s : set π} :
has_deriv_within_at f f' s x β unique_diff_within_at π s x β deriv_within f s x = f'
theorem
fderiv_within_deriv_within
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s : set π} :
β(fderiv_within π f s x) 1 = deriv_within f s x
theorem
deriv_within_fderiv_within
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s : set π} :
1.smul_right (deriv_within f s x) = fderiv_within π f s x
theorem
fderiv_deriv
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π} :
theorem
deriv_fderiv
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π} :
1.smul_right (deriv f x) = fderiv π f x
theorem
differentiable_at.deriv_within
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s : set π} :
differentiable_at π f x β unique_diff_within_at π s x β deriv_within f s x = deriv f x
theorem
deriv_within_subset
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s t : set π} :
s β t β unique_diff_within_at π s x β differentiable_within_at π f t x β deriv_within f s x = deriv_within f t x
@[simp]
theorem
deriv_within_univ
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F} :
deriv_within f set.univ = deriv f
theorem
deriv_within_inter
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s t : set π} :
t β nhds x β unique_diff_within_at π s x β deriv_within f (s β© t) x = deriv_within f s x
Congruence properties of derivatives
theorem
filter.eventually_eq.has_deriv_at_filter_iff
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{fβ fβ : π β F}
{fβ' fβ' : F}
{x : π}
{L : filter π} :
fβ =αΆ [L] fβ β fβ x = fβ x β fβ' = fβ' β (has_deriv_at_filter fβ fβ' x L β has_deriv_at_filter fβ fβ' x L)
theorem
has_deriv_at_filter.congr_of_eventually_eq
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f fβ : π β F}
{f' : F}
{x : π}
{L : filter π} :
has_deriv_at_filter f f' x L β fβ =αΆ [L] f β fβ x = f x β has_deriv_at_filter fβ f' x L
theorem
has_deriv_within_at.congr_mono
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f fβ : π β F}
{f' : F}
{x : π}
{s t : set π} :
has_deriv_within_at f f' s x β (β (x : π), x β t β fβ x = f x) β fβ x = f x β t β s β has_deriv_within_at fβ f' t x
theorem
has_deriv_within_at.congr
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f fβ : π β F}
{f' : F}
{x : π}
{s : set π} :
has_deriv_within_at f f' s x β (β (x : π), x β s β fβ x = f x) β fβ x = f x β has_deriv_within_at fβ f' s x
theorem
has_deriv_within_at.congr_of_eventually_eq
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f fβ : π β F}
{f' : F}
{x : π}
{s : set π} :
has_deriv_within_at f f' s x β fβ =αΆ [nhds_within x s] f β fβ x = f x β has_deriv_within_at fβ f' s x
theorem
has_deriv_at.congr_of_eventually_eq
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f fβ : π β F}
{f' : F}
{x : π} :
has_deriv_at f f' x β fβ =αΆ [nhds x] f β has_deriv_at fβ f' x
theorem
filter.eventually_eq.deriv_within_eq
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f fβ : π β F}
{x : π}
{s : set π} :
unique_diff_within_at π s x β fβ =αΆ [nhds_within x s] f β fβ x = f x β deriv_within fβ s x = deriv_within f s x
theorem
deriv_within_congr
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f fβ : π β F}
{x : π}
{s : set π} :
unique_diff_within_at π s x β (β (y : π), y β s β fβ y = f y) β fβ x = f x β deriv_within fβ s x = deriv_within f s x
theorem
filter.eventually_eq.deriv_eq
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f fβ : π β F}
{x : π} :
Derivative of the identity
theorem
has_deriv_at_filter_id
{π : Type u}
[nondiscrete_normed_field π]
(x : π)
(L : filter π) :
has_deriv_at_filter id 1 x L
theorem
has_deriv_within_at_id
{π : Type u}
[nondiscrete_normed_field π]
(x : π)
(s : set π) :
has_deriv_within_at id 1 s x
theorem
has_deriv_at_id
{π : Type u}
[nondiscrete_normed_field π]
(x : π) :
has_deriv_at id 1 x
theorem
has_deriv_at_id'
{π : Type u}
[nondiscrete_normed_field π]
(x : π) :
has_deriv_at (Ξ» (x : π), x) 1 x
@[simp]
theorem
deriv_within_id
{π : Type u}
[nondiscrete_normed_field π]
(x : π)
(s : set π) :
unique_diff_within_at π s x β deriv_within id s x = 1
Derivative of constant functions
theorem
has_deriv_at_filter_const
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
(x : π)
(L : filter π)
(c : F) :
has_deriv_at_filter (Ξ» (x : π), c) 0 x L
theorem
has_strict_deriv_at_const
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
(x : π)
(c : F) :
has_strict_deriv_at (Ξ» (x : π), c) 0 x
theorem
has_deriv_within_at_const
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
(x : π)
(s : set π)
(c : F) :
has_deriv_within_at (Ξ» (x : π), c) 0 s x
theorem
has_deriv_at_const
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
(x : π)
(c : F) :
has_deriv_at (Ξ» (x : π), c) 0 x
theorem
deriv_const
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
(x : π)
(c : F) :
@[simp]
theorem
deriv_const'
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
(c : F) :
theorem
deriv_within_const
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
(x : π)
(s : set π)
(c : F) :
unique_diff_within_at π s x β deriv_within (Ξ» (x : π), c) s x = 0
Derivative of continuous linear maps
theorem
continuous_linear_map.has_deriv_at_filter
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{x : π}
{L : filter π}
(e : π βL[π] F) :
has_deriv_at_filter βe (βe 1) x L
theorem
continuous_linear_map.has_strict_deriv_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{x : π}
(e : π βL[π] F) :
has_strict_deriv_at βe (βe 1) x
theorem
continuous_linear_map.has_deriv_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{x : π}
(e : π βL[π] F) :
has_deriv_at βe (βe 1) x
theorem
continuous_linear_map.has_deriv_within_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{x : π}
{s : set π}
(e : π βL[π] F) :
has_deriv_within_at βe (βe 1) s x
@[simp]
theorem
continuous_linear_map.deriv
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{x : π}
(e : π βL[π] F) :
theorem
continuous_linear_map.deriv_within
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{x : π}
{s : set π}
(e : π βL[π] F) :
unique_diff_within_at π s x β deriv_within βe s x = βe 1
Derivative of bundled linear maps
theorem
linear_map.has_deriv_at_filter
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{x : π}
{L : filter π}
(e : π ββ[π] F) :
has_deriv_at_filter βe (βe 1) x L
theorem
linear_map.has_strict_deriv_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{x : π}
(e : π ββ[π] F) :
has_strict_deriv_at βe (βe 1) x
theorem
linear_map.has_deriv_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{x : π}
(e : π ββ[π] F) :
has_deriv_at βe (βe 1) x
theorem
linear_map.has_deriv_within_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{x : π}
{s : set π}
(e : π ββ[π] F) :
has_deriv_within_at βe (βe 1) s x
@[simp]
theorem
linear_map.deriv
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{x : π}
(e : π ββ[π] F) :
theorem
linear_map.deriv_within
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{x : π}
{s : set π}
(e : π ββ[π] F) :
unique_diff_within_at π s x β deriv_within βe s x = βe 1
Derivative of the sum of two functions
theorem
has_deriv_at_filter.add
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f g : π β F}
{f' g' : F}
{x : π}
{L : filter π} :
has_deriv_at_filter f f' x L β 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}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f g : π β F}
{f' g' : F}
{x : π} :
has_strict_deriv_at f f' x β 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}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f g : π β F}
{f' g' : F}
{x : π}
{s : set π} :
has_deriv_within_at f f' s x β 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}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f g : π β F}
{f' g' : F}
{x : π} :
has_deriv_at f f' x β has_deriv_at g g' x β has_deriv_at (Ξ» (x : π), f x + g x) (f' + g') x
theorem
deriv_within_add
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f g : π β F}
{x : π}
{s : set π} :
unique_diff_within_at π s x β differentiable_within_at π f s x β 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}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f g : π β F}
{x : π} :
differentiable_at π f x β differentiable_at π g x β deriv (Ξ» (y : π), f y + g y) x = deriv f x + deriv g x
theorem
has_deriv_at_filter.add_const
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_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}
[nondiscrete_normed_field π]
{F : Type v}
[normed_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}
[nondiscrete_normed_field π]
{F : Type v}
[normed_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}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s : set π}
(hxs : unique_diff_within_at π s x)
(hf : differentiable_within_at π f s x)
(c : F) :
deriv_within (Ξ» (y : π), f y + c) s x = deriv_within f s x
theorem
deriv_add_const
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
(hf : differentiable_at π f x)
(c : F) :
theorem
has_deriv_at_filter.const_add
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{L : filter π}
(c : F) :
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}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s : set π}
(c : F) :
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}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
(c : F) :
has_deriv_at f f' x β has_deriv_at (Ξ» (x : π), c + f x) f' x
theorem
deriv_within_const_add
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s : set π}
(hxs : unique_diff_within_at π s x)
(c : F) :
differentiable_within_at π f s x β deriv_within (Ξ» (y : π), c + f y) s x = deriv_within f s x
theorem
deriv_const_add
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
(c : F) :
differentiable_at π f x β deriv (Ξ» (y : π), c + f y) x = deriv f x
Derivative of a finite sum of functions
theorem
has_deriv_at_filter.sum
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{x : π}
{L : filter π}
{ΞΉ : Type u_1}
{u : finset ΞΉ}
{A : ΞΉ β π β F}
{A' : ΞΉ β F} :
(β (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}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{x : π}
{ΞΉ : Type u_1}
{u : finset ΞΉ}
{A : ΞΉ β π β F}
{A' : ΞΉ β F} :
(β (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}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{x : π}
{s : set π}
{ΞΉ : Type u_1}
{u : finset ΞΉ}
{A : ΞΉ β π β F}
{A' : ΞΉ β F} :
(β (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}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{x : π}
{ΞΉ : Type u_1}
{u : finset ΞΉ}
{A : ΞΉ β π β F}
{A' : ΞΉ β F} :
(β (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}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{x : π}
{s : set π}
{ΞΉ : Type u_1}
{u : finset ΞΉ}
{A : ΞΉ β π β F} :
unique_diff_within_at π s x β (β (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}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{x : π}
{ΞΉ : Type u_1}
{u : finset ΞΉ}
{A : ΞΉ β π β F} :
Derivative of the multiplication of a scalar function and a vector function
theorem
has_deriv_within_at.smul
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s : set π}
{c : π β π}
{c' : π} :
has_deriv_within_at c c' s x β has_deriv_within_at f f' s x β has_deriv_within_at (Ξ» (y : π), c y β’ f y) (c x β’ f' + c' β’ f x) s x
theorem
has_deriv_at.smul
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{c : π β π}
{c' : π} :
has_deriv_at c c' x β has_deriv_at f f' x β has_deriv_at (Ξ» (y : π), c y β’ f y) (c x β’ f' + c' β’ f x) x
theorem
has_strict_deriv_at.smul
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{c : π β π}
{c' : π} :
has_strict_deriv_at c c' x β has_strict_deriv_at f f' x β has_strict_deriv_at (Ξ» (y : π), c y β’ f y) (c x β’ f' + c' β’ f x) x
theorem
deriv_within_smul
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s : set π}
{c : π β π} :
unique_diff_within_at π s x β differentiable_within_at π c s x β differentiable_within_at π f s x β deriv_within (Ξ» (y : π), c y β’ f y) s x = c x β’ deriv_within f s x + deriv_within c s x β’ f x
theorem
deriv_smul
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
{c : π β π} :
differentiable_at π c x β differentiable_at π f x β deriv (Ξ» (y : π), c y β’ f y) x = c x β’ deriv f x + deriv c x β’ f x
theorem
has_deriv_within_at.smul_const
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{x : π}
{s : set π}
{c : π β π}
{c' : π}
(hc : has_deriv_within_at c c' s x)
(f : F) :
has_deriv_within_at (Ξ» (y : π), c y β’ f) (c' β’ f) s x
theorem
has_deriv_at.smul_const
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{x : π}
{c : π β π}
{c' : π}
(hc : has_deriv_at c c' x)
(f : F) :
has_deriv_at (Ξ» (y : π), c y β’ f) (c' β’ f) x
theorem
deriv_within_smul_const
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{x : π}
{s : set π}
{c : π β π}
(hxs : unique_diff_within_at π s x)
(hc : differentiable_within_at π c s x)
(f : F) :
deriv_within (Ξ» (y : π), c y β’ f) s x = deriv_within c s x β’ f
theorem
deriv_smul_const
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{x : π}
{c : π β π}
(hc : differentiable_at π c x)
(f : F) :
theorem
has_deriv_within_at.const_smul
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s : set π}
(c : π) :
has_deriv_within_at f f' s x β has_deriv_within_at (Ξ» (y : π), c β’ f y) (c β’ f') s x
theorem
has_deriv_at.const_smul
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
(c : π) :
has_deriv_at f f' x β has_deriv_at (Ξ» (y : π), c β’ f y) (c β’ f') x
theorem
deriv_within_const_smul
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s : set π}
(hxs : unique_diff_within_at π s x)
(c : π) :
differentiable_within_at π f s x β deriv_within (Ξ» (y : π), c β’ f y) s x = c β’ deriv_within f s x
theorem
deriv_const_smul
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
(c : π) :
Derivative of the negative of a function
theorem
has_deriv_at_filter.neg
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{L : filter π} :
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}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s : set π} :
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}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π} :
has_deriv_at f f' x β has_deriv_at (Ξ» (x : π), -f x) (-f') x
theorem
has_strict_deriv_at.neg
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π} :
has_strict_deriv_at f f' x β has_strict_deriv_at (Ξ» (x : π), -f x) (-f') x
theorem
deriv_within.neg
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s : set π} :
unique_diff_within_at π s x β differentiable_within_at π f s x β deriv_within (Ξ» (y : π), -f y) s x = -deriv_within f s x
theorem
deriv.neg
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π} :
@[simp]
theorem
deriv.neg'
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_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}
[nondiscrete_normed_field π]
(x : π)
(L : filter π) :
has_deriv_at_filter has_neg.neg (-1) x L
theorem
has_deriv_within_at_neg
{π : Type u}
[nondiscrete_normed_field π]
(x : π)
(s : set π) :
has_deriv_within_at has_neg.neg (-1) s x
theorem
has_deriv_at_neg
{π : Type u}
[nondiscrete_normed_field π]
(x : π) :
has_deriv_at has_neg.neg (-1) x
theorem
has_deriv_at_neg'
{π : Type u}
[nondiscrete_normed_field π]
(x : π) :
has_deriv_at (Ξ» (x : π), -x) (-1) x
theorem
has_strict_deriv_at_neg
{π : Type u}
[nondiscrete_normed_field π]
(x : π) :
has_strict_deriv_at has_neg.neg (-1) x
theorem
deriv_neg
{π : Type u}
[nondiscrete_normed_field π]
(x : π) :
deriv has_neg.neg x = -1
@[simp]
theorem
deriv_neg'
{π : Type u}
[nondiscrete_normed_field π] :
deriv has_neg.neg = Ξ» (_x : π), -1
@[simp]
theorem
deriv_within_neg
{π : Type u}
[nondiscrete_normed_field π]
(x : π)
(s : set π) :
unique_diff_within_at π s x β deriv_within has_neg.neg s x = -1
theorem
differentiable_on_neg
{π : Type u}
[nondiscrete_normed_field π]
(s : set π) :
differentiable_on π has_neg.neg s
Derivative of the difference of two functions
theorem
has_deriv_at_filter.sub
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f g : π β F}
{f' g' : F}
{x : π}
{L : filter π} :
has_deriv_at_filter f f' x L β 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}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f g : π β F}
{f' g' : F}
{x : π}
{s : set π} :
has_deriv_within_at f f' s x β 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}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f g : π β F}
{f' g' : F}
{x : π} :
has_deriv_at f f' x β 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}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f g : π β F}
{f' g' : F}
{x : π} :
has_strict_deriv_at f f' x β 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}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f g : π β F}
{x : π}
{s : set π} :
unique_diff_within_at π s x β differentiable_within_at π f s x β 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}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f g : π β F}
{x : π} :
differentiable_at π f x β differentiable_at π g x β deriv (Ξ» (y : π), f y - g y) x = deriv f x - deriv g x
theorem
has_deriv_at_filter.is_O_sub
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{L : filter π} :
has_deriv_at_filter f f' x L β asymptotics.is_O (Ξ» (x' : π), f x' - f x) (Ξ» (x' : π), x' - x) L
theorem
has_deriv_at_filter.sub_const
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_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}
[nondiscrete_normed_field π]
{F : Type v}
[normed_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}
[nondiscrete_normed_field π]
{F : Type v}
[normed_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}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s : set π}
(hxs : unique_diff_within_at π s x)
(hf : differentiable_within_at π f s x)
(c : F) :
deriv_within (Ξ» (y : π), f y - c) s x = deriv_within f s x
theorem
deriv_sub_const
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
(c : F) :
differentiable_at π f x β deriv (Ξ» (y : π), f y - c) x = deriv f x
theorem
has_deriv_at_filter.const_sub
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{L : filter π}
(c : F) :
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}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s : set π}
(c : F) :
has_deriv_within_at f f' s x β has_deriv_within_at (Ξ» (x : π), c - f x) (-f') s x
theorem
has_deriv_at.const_sub
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
(c : F) :
has_deriv_at f f' x β has_deriv_at (Ξ» (x : π), c - f x) (-f') x
theorem
deriv_within_const_sub
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s : set π}
(hxs : unique_diff_within_at π s x)
(c : F) :
differentiable_within_at π f s x β deriv_within (Ξ» (y : π), c - f y) s x = -deriv_within f s x
theorem
deriv_const_sub
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{x : π}
(c : F) :
Continuity of a function admitting a derivative
theorem
has_deriv_at_filter.tendsto_nhds
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{L : filter π} :
L β€ nhds x β has_deriv_at_filter f f' x L β filter.tendsto f L (nhds (f x))
theorem
has_deriv_within_at.continuous_within_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s : set π} :
has_deriv_within_at f f' s x β continuous_within_at f s x
theorem
has_deriv_at.continuous_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π} :
has_deriv_at f f' x β continuous_at f x
Derivative of the cartesian product of two functions
theorem
has_deriv_at_filter.prod
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{fβ : π β F}
{fβ' : F}
{x : π}
{L : filter π}
{G : Type w}
[normed_group G]
[normed_space π G]
{fβ : π β G}
{fβ' : G} :
has_deriv_at_filter fβ fβ' x L β has_deriv_at_filter fβ fβ' x L β has_deriv_at_filter (Ξ» (x : π), (fβ x, fβ x)) (fβ', fβ') x L
theorem
has_deriv_within_at.prod
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{fβ : π β F}
{fβ' : F}
{x : π}
{s : set π}
{G : Type w}
[normed_group G]
[normed_space π G]
{fβ : π β G}
{fβ' : G} :
has_deriv_within_at fβ fβ' s x β has_deriv_within_at fβ fβ' s x β has_deriv_within_at (Ξ» (x : π), (fβ x, fβ x)) (fβ', fβ') s x
theorem
has_deriv_at.prod
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{fβ : π β F}
{fβ' : F}
{x : π}
{G : Type w}
[normed_group G]
[normed_space π G]
{fβ : π β G}
{fβ' : G} :
has_deriv_at fβ fβ' x β has_deriv_at fβ fβ' x β has_deriv_at (Ξ» (x : π), (fβ x, fβ x)) (fβ', fβ') x
Derivative of the composition of a vector function and a scalar function
We use scomp in lemmas on composition of vector valued and scalar valued functions, and comp
in lemmas on composition of scalar valued functions, in analogy for smul and mul (and also
because the comp version with the shorter name will show up much more often in applications).
The formula for the derivative involves smul in scomp lemmas, which can be reduced to
usual multiplication in comp lemmas.
theorem
has_deriv_at_filter.scomp
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{g : π β F}
{g' : F}
(x : π)
{L : filter π}
{h : π β π}
{h' : π} :
has_deriv_at_filter g g' (h x) (filter.map h L) β has_deriv_at_filter h h' x L β has_deriv_at_filter (g β h) (h' β’ g') x L
theorem
has_deriv_within_at.scomp
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{g : π β F}
{g' : F}
(x : π)
{s : set π}
{h : π β π}
{h' : π}
{t : set π} :
has_deriv_within_at g g' t (h x) β has_deriv_within_at h h' s x β s β h β»ΒΉ' t β has_deriv_within_at (g β h) (h' β’ g') s x
theorem
has_deriv_at.scomp
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{g : π β F}
{g' : F}
(x : π)
{h : π β π}
{h' : π} :
has_deriv_at g g' (h x) β has_deriv_at h h' x β has_deriv_at (g β h) (h' β’ g') x
The chain rule.
theorem
has_strict_deriv_at.scomp
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{g : π β F}
{g' : F}
(x : π)
{h : π β π}
{h' : π} :
has_strict_deriv_at g g' (h x) β has_strict_deriv_at h h' x β has_strict_deriv_at (g β h) (h' β’ g') x
theorem
has_deriv_at.scomp_has_deriv_within_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{g : π β F}
{g' : F}
(x : π)
{s : set π}
{h : π β π}
{h' : π} :
has_deriv_at g g' (h x) β has_deriv_within_at h h' s x β has_deriv_within_at (g β h) (h' β’ g') s x
theorem
deriv_within.scomp
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{g : π β F}
(x : π)
{s t : set π}
{h : π β π} :
differentiable_within_at π g t (h x) β differentiable_within_at π h s x β s β h β»ΒΉ' t β unique_diff_within_at π s x β deriv_within (g β h) s x = deriv_within h s x β’ deriv_within g t (h x)
theorem
deriv.scomp
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{g : π β F}
(x : π)
{h : π β π} :
differentiable_at π g (h x) β differentiable_at π h x β deriv (g β h) x = deriv h x β’ deriv g (h x)
Derivative of the composition of two scalar functions
theorem
has_deriv_at_filter.comp
{π : Type u}
[nondiscrete_normed_field π]
(x : π)
{L : filter π}
{hβ hβ : π β π}
{hβ' hβ' : π} :
has_deriv_at_filter hβ hβ' (hβ x) (filter.map hβ L) β has_deriv_at_filter hβ hβ' x L β has_deriv_at_filter (hβ β hβ) (hβ' * hβ') x L
theorem
has_deriv_within_at.comp
{π : Type u}
[nondiscrete_normed_field π]
(x : π)
{s : set π}
{hβ hβ : π β π}
{hβ' hβ' : π}
{t : set π} :
has_deriv_within_at hβ hβ' t (hβ x) β has_deriv_within_at hβ hβ' s x β s β hβ β»ΒΉ' t β has_deriv_within_at (hβ β hβ) (hβ' * hβ') s x
theorem
has_deriv_at.comp
{π : Type u}
[nondiscrete_normed_field π]
(x : π)
{hβ hβ : π β π}
{hβ' hβ' : π} :
has_deriv_at hβ hβ' (hβ x) β has_deriv_at hβ hβ' x β has_deriv_at (hβ β hβ) (hβ' * hβ') x
The chain rule.
theorem
has_strict_deriv_at.comp
{π : Type u}
[nondiscrete_normed_field π]
(x : π)
{hβ hβ : π β π}
{hβ' hβ' : π} :
has_strict_deriv_at hβ hβ' (hβ x) β has_strict_deriv_at hβ hβ' x β has_strict_deriv_at (hβ β hβ) (hβ' * hβ') x
theorem
has_deriv_at.comp_has_deriv_within_at
{π : Type u}
[nondiscrete_normed_field π]
(x : π)
{s : set π}
{hβ hβ : π β π}
{hβ' hβ' : π} :
has_deriv_at hβ hβ' (hβ x) β has_deriv_within_at hβ hβ' s x β has_deriv_within_at (hβ β hβ) (hβ' * hβ') s x
theorem
deriv_within.comp
{π : Type u}
[nondiscrete_normed_field π]
(x : π)
{s t : set π}
{hβ hβ : π β π} :
differentiable_within_at π hβ t (hβ x) β differentiable_within_at π hβ s x β s β hβ β»ΒΉ' t β unique_diff_within_at π s x β deriv_within (hβ β hβ) s x = deriv_within hβ t (hβ x) * deriv_within hβ s x
theorem
deriv.comp
{π : Type u}
[nondiscrete_normed_field π]
(x : π)
{hβ hβ : π β π} :
differentiable_at π hβ (hβ x) β differentiable_at π hβ x β deriv (hβ β hβ) x = deriv hβ (hβ x) * deriv hβ x
theorem
has_deriv_at_filter.iterate
{π : Type u}
[nondiscrete_normed_field π]
(x : π)
{L : filter π}
{f : π β π}
{f' : π}
(hf : has_deriv_at_filter f f' x L)
(hL : filter.tendsto f L L)
(hx : f x = x)
(n : β) :
has_deriv_at_filter f^[n] (f' ^ n) x L
theorem
has_deriv_at.iterate
{π : Type u}
[nondiscrete_normed_field π]
(x : π)
{f : π β π}
{f' : π}
(hf : has_deriv_at f f' x)
(hx : f x = x)
(n : β) :
has_deriv_at f^[n] (f' ^ n) x
theorem
has_deriv_within_at.iterate
{π : Type u}
[nondiscrete_normed_field π]
(x : π)
{s : set π}
{f : π β π}
{f' : π}
(hf : has_deriv_within_at f f' s x)
(hx : f x = x)
(hs : set.maps_to f s s)
(n : β) :
has_deriv_within_at f^[n] (f' ^ n) s x
theorem
has_strict_deriv_at.iterate
{π : Type u}
[nondiscrete_normed_field π]
(x : π)
{f : π β π}
{f' : π}
(hf : has_strict_deriv_at f f' x)
(hx : f x = x)
(n : β) :
has_strict_deriv_at f^[n] (f' ^ n) x
Derivative of the composition of a function between vector spaces and of a function defined on π
theorem
has_fderiv_within_at.comp_has_deriv_within_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{E : Type w}
[normed_group E]
[normed_space π E]
{f : π β F}
{f' : F}
(x : π)
{s : set π}
{l : F β E}
{l' : F βL[π] E}
{t : set F} :
has_fderiv_within_at l l' t (f x) β has_deriv_within_at f f' s x β s β f β»ΒΉ' t β has_deriv_within_at (l β f) (βl' f') s x
The composition l β f where l : F β E and f : π β F, has a derivative within a set
equal to the FrΓ©chet derivative of l applied to the derivative of f.
theorem
has_fderiv_at.comp_has_deriv_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{E : Type w}
[normed_group E]
[normed_space π E]
{f : π β F}
{f' : F}
(x : π)
{l : F β E}
{l' : F βL[π] E} :
has_fderiv_at l l' (f x) β has_deriv_at f f' x β has_deriv_at (l β f) (βl' f') x
The composition l β f where l : F β E and f : π β F, has a derivative equal to the
FrΓ©chet derivative of l applied to the derivative of f.
theorem
has_fderiv_at.comp_has_deriv_within_at
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{E : Type w}
[normed_group E]
[normed_space π E]
{f : π β F}
{f' : F}
(x : π)
{s : set π}
{l : F β E}
{l' : F βL[π] E} :
has_fderiv_at l l' (f x) β has_deriv_within_at f f' s x β has_deriv_within_at (l β f) (βl' f') s x
theorem
fderiv_within.comp_deriv_within
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{E : Type w}
[normed_group E]
[normed_space π E]
{f : π β F}
(x : π)
{s : set π}
{l : F β E}
{t : set F} :
differentiable_within_at π l t (f x) β differentiable_within_at π f s x β s β f β»ΒΉ' t β unique_diff_within_at π s x β deriv_within (l β f) s x = β(fderiv_within π l t (f x)) (deriv_within f s x)
theorem
fderiv.comp_deriv
{π : Type u}
[nondiscrete_normed_field π]
{F : Type v}
[normed_group F]
[normed_space π F]
{E : Type w}
[normed_group E]
[normed_space π E]
{f : π β F}
(x : π)
{l : F β E} :
differentiable_at π l (f x) β differentiable_at π f x β deriv (l β f) x = β(fderiv π l (f x)) (deriv f x)
Derivative of the multiplication of two scalar functions
theorem
has_deriv_within_at.mul
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{s : set π}
{c d : π β π}
{c' d' : π} :
has_deriv_within_at c c' s x β has_deriv_within_at d d' s x β has_deriv_within_at (Ξ» (y : π), c y * d y) (c' * d x + c x * d') s x
theorem
has_deriv_at.mul
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{c d : π β π}
{c' d' : π} :
has_deriv_at c c' x β has_deriv_at d d' x β has_deriv_at (Ξ» (y : π), c y * d y) (c' * d x + c x * d') x
theorem
has_strict_deriv_at.mul
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{c d : π β π}
{c' d' : π} :
has_strict_deriv_at c c' x β has_strict_deriv_at d d' x β has_strict_deriv_at (Ξ» (y : π), c y * d y) (c' * d x + c x * d') x
theorem
deriv_within_mul
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{s : set π}
{c d : π β π} :
unique_diff_within_at π s x β differentiable_within_at π c s x β differentiable_within_at π d s x β deriv_within (Ξ» (y : π), c y * d y) s x = deriv_within c s x * d x + c x * deriv_within d s x
@[simp]
theorem
deriv_mul
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{c d : π β π} :
differentiable_at π c x β differentiable_at π d x β deriv (Ξ» (y : π), c y * d y) x = deriv c x * d x + c x * deriv d x
theorem
has_deriv_within_at.mul_const
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{s : set π}
{c : π β π}
{c' : π}
(hc : has_deriv_within_at c c' s x)
(d : π) :
has_deriv_within_at (Ξ» (y : π), c y * d) (c' * d) s x
theorem
has_deriv_at.mul_const
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{c : π β π}
{c' : π}
(hc : has_deriv_at c c' x)
(d : π) :
has_deriv_at (Ξ» (y : π), c y * d) (c' * d) x
theorem
deriv_within_mul_const
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{s : set π}
{c : π β π}
(hxs : unique_diff_within_at π s x)
(hc : differentiable_within_at π c s x)
(d : π) :
deriv_within (Ξ» (y : π), c y * d) s x = deriv_within c s x * d
theorem
deriv_mul_const
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{c : π β π}
(hc : differentiable_at π c x)
(d : π) :
theorem
has_deriv_within_at.const_mul
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{s : set π}
{d : π β π}
{d' : π}
(c : π) :
has_deriv_within_at d d' s x β has_deriv_within_at (Ξ» (y : π), c * d y) (c * d') s x
theorem
has_deriv_at.const_mul
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{d : π β π}
{d' : π}
(c : π) :
has_deriv_at d d' x β has_deriv_at (Ξ» (y : π), c * d y) (c * d') x
theorem
deriv_within_const_mul
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{s : set π}
{d : π β π}
(hxs : unique_diff_within_at π s x)
(c : π) :
differentiable_within_at π d s x β deriv_within (Ξ» (y : π), c * d y) s x = c * deriv_within d s x
theorem
deriv_const_mul
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{d : π β π}
(c : π) :
Derivative of x β¦ xβ»ΒΉ
theorem
has_strict_deriv_at_inv
{π : Type u}
[nondiscrete_normed_field π]
{x : π} :
x β 0 β has_strict_deriv_at has_inv.inv (-(x ^ 2)β»ΒΉ) x
theorem
has_deriv_within_at_inv
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
(x_ne_zero : x β 0)
(s : set π) :
has_deriv_within_at (Ξ» (x : π), xβ»ΒΉ) (-(x ^ 2)β»ΒΉ) s x
theorem
differentiable_at_inv
{π : Type u}
[nondiscrete_normed_field π]
{x : π} :
x β 0 β differentiable_at π (Ξ» (x : π), xβ»ΒΉ) x
theorem
differentiable_within_at_inv
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{s : set π} :
x β 0 β differentiable_within_at π (Ξ» (x : π), xβ»ΒΉ) s x
theorem
differentiable_on_inv
{π : Type u}
[nondiscrete_normed_field π] :
differentiable_on π (Ξ» (x : π), xβ»ΒΉ) {x : π | x β 0}
theorem
deriv_within_inv
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{s : set π} :
x β 0 β unique_diff_within_at π s x β deriv_within (Ξ» (x : π), xβ»ΒΉ) s x = -(x ^ 2)β»ΒΉ
theorem
has_fderiv_at_inv
{π : Type u}
[nondiscrete_normed_field π]
{x : π} :
x β 0 β has_fderiv_at (Ξ» (x : π), xβ»ΒΉ) (1.smul_right (-(x ^ 2)β»ΒΉ)) x
theorem
has_fderiv_within_at_inv
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{s : set π} :
x β 0 β has_fderiv_within_at (Ξ» (x : π), xβ»ΒΉ) (1.smul_right (-(x ^ 2)β»ΒΉ)) s x
theorem
fderiv_within_inv
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{s : set π} :
x β 0 β unique_diff_within_at π s x β fderiv_within π (Ξ» (x : π), xβ»ΒΉ) s x = 1.smul_right (-(x ^ 2)β»ΒΉ)
theorem
has_deriv_within_at.inv
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{s : set π}
{c : π β π}
{c' : π} :
has_deriv_within_at c c' s x β c x β 0 β has_deriv_within_at (Ξ» (y : π), (c y)β»ΒΉ) (-c' / c x ^ 2) s x
theorem
has_deriv_at.inv
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{c : π β π}
{c' : π} :
has_deriv_at c c' x β c x β 0 β has_deriv_at (Ξ» (y : π), (c y)β»ΒΉ) (-c' / c x ^ 2) x
theorem
differentiable_within_at.inv
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{s : set π}
{c : π β π} :
differentiable_within_at π c s x β c x β 0 β differentiable_within_at π (Ξ» (x : π), (c x)β»ΒΉ) s x
@[simp]
theorem
differentiable_at.inv
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{c : π β π} :
differentiable_at π c x β c x β 0 β differentiable_at π (Ξ» (x : π), (c x)β»ΒΉ) x
theorem
differentiable_on.inv
{π : Type u}
[nondiscrete_normed_field π]
{s : set π}
{c : π β π} :
differentiable_on π c s β (β (x : π), x β s β c x β 0) β differentiable_on π (Ξ» (x : π), (c x)β»ΒΉ) s
@[simp]
theorem
differentiable.inv
{π : Type u}
[nondiscrete_normed_field π]
{c : π β π} :
differentiable π c β (β (x : π), c x β 0) β differentiable π (Ξ» (x : π), (c x)β»ΒΉ)
theorem
deriv_within_inv'
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{s : set π}
{c : π β π} :
differentiable_within_at π c s x β c x β 0 β unique_diff_within_at π s x β deriv_within (Ξ» (x : π), (c x)β»ΒΉ) s x = -deriv_within c s x / c x ^ 2
@[simp]
Derivative of x β¦ c x / d x
theorem
has_deriv_within_at.div
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{s : set π}
{c d : π β π}
{c' d' : π} :
has_deriv_within_at c c' s x β has_deriv_within_at d d' s x β d x β 0 β has_deriv_within_at (Ξ» (y : π), c y / d y) ((c' * d x - c x * d') / d x ^ 2) s x
theorem
has_deriv_at.div
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{c d : π β π}
{c' d' : π} :
has_deriv_at c c' x β has_deriv_at d d' x β d x β 0 β has_deriv_at (Ξ» (y : π), c y / d y) ((c' * d x - c x * d') / d x ^ 2) x
theorem
differentiable_within_at.div
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{s : set π}
{c d : π β π} :
differentiable_within_at π c s x β differentiable_within_at π d s x β d x β 0 β differentiable_within_at π (Ξ» (x : π), c x / d x) s x
@[simp]
theorem
differentiable_at.div
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{c d : π β π} :
differentiable_at π c x β differentiable_at π d x β d x β 0 β differentiable_at π (Ξ» (x : π), c x / d x) x
theorem
differentiable_on.div
{π : Type u}
[nondiscrete_normed_field π]
{s : set π}
{c d : π β π} :
differentiable_on π c s β differentiable_on π d s β (β (x : π), x β s β d x β 0) β differentiable_on π (Ξ» (x : π), c x / d x) s
@[simp]
theorem
differentiable.div
{π : Type u}
[nondiscrete_normed_field π]
{c d : π β π} :
differentiable π c β differentiable π d β (β (x : π), d x β 0) β differentiable π (Ξ» (x : π), c x / d x)
theorem
deriv_within_div
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{s : set π}
{c d : π β π} :
differentiable_within_at π c s x β differentiable_within_at π d s x β d x β 0 β unique_diff_within_at π s x β deriv_within (Ξ» (x : π), c x / d x) s x = (deriv_within c s x * d x - c x * deriv_within d s x) / d x ^ 2
theorem
differentiable_within_at.div_const
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{s : set π}
{c : π β π}
(hc : differentiable_within_at π c s x)
{d : π} :
differentiable_within_at π (Ξ» (x : π), c x / d) s x
@[simp]
theorem
differentiable_at.div_const
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{c : π β π}
(hc : differentiable_at π c x)
{d : π} :
differentiable_at π (Ξ» (x : π), c x / d) x
theorem
differentiable_on.div_const
{π : Type u}
[nondiscrete_normed_field π]
{s : set π}
{c : π β π}
(hc : differentiable_on π c s)
{d : π} :
differentiable_on π (Ξ» (x : π), c x / d) s
@[simp]
theorem
differentiable.div_const
{π : Type u}
[nondiscrete_normed_field π]
{c : π β π}
(hc : differentiable π c)
{d : π} :
differentiable π (Ξ» (x : π), c x / d)
theorem
deriv_within_div_const
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{s : set π}
{c : π β π}
(hc : differentiable_within_at π c s x)
{d : π} :
unique_diff_within_at π s x β deriv_within (Ξ» (x : π), c x / d) s x = deriv_within c s x / d
@[simp]
theorem
deriv_div_const
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{c : π β π}
(hc : differentiable_at π c x)
{d : π} :
theorem
has_strict_deriv_at.has_strict_fderiv_at_equiv
{π : Type u}
[nondiscrete_normed_field π]
{f : π β π}
{f' x : π}
(hf : has_strict_deriv_at f f' x)
(hf' : f' β 0) :
has_strict_fderiv_at f β(β(continuous_linear_equiv.units_equiv_aut π) (units.mk0 f' hf')) x
theorem
has_deriv_at.has_fderiv_at_equiv
{π : Type u}
[nondiscrete_normed_field π]
{f : π β π}
{f' x : π}
(hf : has_deriv_at f f' x)
(hf' : f' β 0) :
has_fderiv_at f β(β(continuous_linear_equiv.units_equiv_aut π) (units.mk0 f' hf')) x
theorem
has_strict_deriv_at.of_local_left_inverse
{π : Type u}
[nondiscrete_normed_field π]
{f g : π β π}
{f' a : π} :
continuous_at g a β has_strict_deriv_at f f' (g a) β f' β 0 β (βαΆ (y : π) in nhds a, f (g y) = y) β has_strict_deriv_at g f'β»ΒΉ a
If f (g y) = y for y in some neighborhood of a, g is continuous at a, and f has an
invertible derivative f' at g a in the strict sense, then g has the derivative f'β»ΒΉ at a
in the strict sense.
This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.
theorem
has_deriv_at.of_local_left_inverse
{π : Type u}
[nondiscrete_normed_field π]
{f g : π β π}
{f' a : π} :
continuous_at g a β has_deriv_at f f' (g a) β f' β 0 β (βαΆ (y : π) in nhds a, f (g y) = y) β has_deriv_at g f'β»ΒΉ a
If f (g y) = y for y in some neighborhood of a, g is continuous at a, and f has an
invertible derivative f' at g a, then g has the derivative f'β»ΒΉ at a.
This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.
Derivative of a polynomial
theorem
polynomial.has_strict_deriv_at
{π : Type u}
[nondiscrete_normed_field π]
(p : polynomial π)
(x : π) :
has_strict_deriv_at (Ξ» (x : π), polynomial.eval x p) (polynomial.eval x p.derivative) x
The derivative (in the analysis sense) of a polynomial p is given by p.derivative.
theorem
polynomial.has_deriv_at
{π : Type u}
[nondiscrete_normed_field π]
(p : polynomial π)
(x : π) :
has_deriv_at (Ξ» (x : π), polynomial.eval x p) (polynomial.eval x p.derivative) x
The derivative (in the analysis sense) of a polynomial p is given by p.derivative.
theorem
polynomial.has_deriv_within_at
{π : Type u}
[nondiscrete_normed_field π]
(p : polynomial π)
(x : π)
(s : set π) :
has_deriv_within_at (Ξ» (x : π), polynomial.eval x p) (polynomial.eval x p.derivative) s x
theorem
polynomial.differentiable_at
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
(p : polynomial π) :
differentiable_at π (Ξ» (x : π), polynomial.eval x p) x
theorem
polynomial.differentiable_within_at
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{s : set π}
(p : polynomial π) :
differentiable_within_at π (Ξ» (x : π), polynomial.eval x p) s x
theorem
polynomial.differentiable
{π : Type u}
[nondiscrete_normed_field π]
(p : polynomial π) :
differentiable π (Ξ» (x : π), polynomial.eval x p)
theorem
polynomial.differentiable_on
{π : Type u}
[nondiscrete_normed_field π]
{s : set π}
(p : polynomial π) :
differentiable_on π (Ξ» (x : π), polynomial.eval x p) s
@[simp]
theorem
polynomial.deriv
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
(p : polynomial π) :
deriv (Ξ» (x : π), polynomial.eval x p) x = polynomial.eval x p.derivative
theorem
polynomial.deriv_within
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{s : set π}
(p : polynomial π) :
unique_diff_within_at π s x β deriv_within (Ξ» (x : π), polynomial.eval x p) s x = polynomial.eval x p.derivative
theorem
polynomial.continuous
{π : Type u}
[nondiscrete_normed_field π]
(p : polynomial π) :
continuous (Ξ» (x : π), polynomial.eval x p)
theorem
polynomial.continuous_on
{π : Type u}
[nondiscrete_normed_field π]
{s : set π}
(p : polynomial π) :
continuous_on (Ξ» (x : π), polynomial.eval x p) s
theorem
polynomial.continuous_at
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
(p : polynomial π) :
continuous_at (Ξ» (x : π), polynomial.eval x p) x
theorem
polynomial.continuous_within_at
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{s : set π}
(p : polynomial π) :
continuous_within_at (Ξ» (x : π), polynomial.eval x p) s x
theorem
polynomial.has_fderiv_at
{π : Type u}
[nondiscrete_normed_field π]
(p : polynomial π)
(x : π) :
has_fderiv_at (Ξ» (x : π), polynomial.eval x p) (1.smul_right (polynomial.eval x p.derivative)) x
theorem
polynomial.has_fderiv_within_at
{π : Type u}
[nondiscrete_normed_field π]
{s : set π}
(p : polynomial π)
(x : π) :
has_fderiv_within_at (Ξ» (x : π), polynomial.eval x p) (1.smul_right (polynomial.eval x p.derivative)) s x
@[simp]
theorem
polynomial.fderiv
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
(p : polynomial π) :
fderiv π (Ξ» (x : π), polynomial.eval x p) x = 1.smul_right (polynomial.eval x p.derivative)
theorem
polynomial.fderiv_within
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{s : set π}
(p : polynomial π) :
unique_diff_within_at π s x β fderiv_within π (Ξ» (x : π), polynomial.eval x p) s x = 1.smul_right (polynomial.eval x p.derivative)
Derivative of x β¦ x^n for n : β
theorem
has_strict_deriv_at_pow
{π : Type u}
[nondiscrete_normed_field π]
(n : β)
(x : π) :
theorem
has_deriv_within_at_pow
{π : Type u}
[nondiscrete_normed_field π]
(n : β)
(x : π)
(s : set π) :
theorem
differentiable_at_pow
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{n : β} :
differentiable_at π (Ξ» (x : π), x ^ n) x
theorem
differentiable_within_at_pow
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{s : set π}
{n : β} :
differentiable_within_at π (Ξ» (x : π), x ^ n) s x
theorem
differentiable_pow
{π : Type u}
[nondiscrete_normed_field π]
{n : β} :
differentiable π (Ξ» (x : π), x ^ n)
theorem
differentiable_on_pow
{π : Type u}
[nondiscrete_normed_field π]
{s : set π}
{n : β} :
differentiable_on π (Ξ» (x : π), x ^ n) s
theorem
deriv_within_pow
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{s : set π}
{n : β} :
unique_diff_within_at π s x β deriv_within (Ξ» (x : π), x ^ n) s x = βn * x ^ (n - 1)
theorem
has_deriv_within_at.pow
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{s : set π}
{c : π β π}
{c' : π}
{n : β} :
has_deriv_within_at c c' s x β has_deriv_within_at (Ξ» (y : π), c y ^ n) (βn * c x ^ (n - 1) * c') s x
theorem
has_deriv_at.pow
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{c : π β π}
{c' : π}
{n : β} :
has_deriv_at c c' x β has_deriv_at (Ξ» (y : π), c y ^ n) (βn * c x ^ (n - 1) * c') x
theorem
differentiable_within_at.pow
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{s : set π}
{c : π β π}
{n : β} :
differentiable_within_at π c s x β differentiable_within_at π (Ξ» (x : π), c x ^ n) s x
@[simp]
theorem
differentiable_at.pow
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{c : π β π}
{n : β} :
differentiable_at π c x β differentiable_at π (Ξ» (x : π), c x ^ n) x
theorem
differentiable_on.pow
{π : Type u}
[nondiscrete_normed_field π]
{s : set π}
{c : π β π}
{n : β} :
differentiable_on π c s β differentiable_on π (Ξ» (x : π), c x ^ n) s
@[simp]
theorem
differentiable.pow
{π : Type u}
[nondiscrete_normed_field π]
{c : π β π}
{n : β} :
differentiable π c β differentiable π (Ξ» (x : π), c x ^ n)
theorem
deriv_within_pow'
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{s : set π}
{c : π β π}
{n : β} :
differentiable_within_at π c s x β unique_diff_within_at π s x β deriv_within (Ξ» (x : π), c x ^ n) s x = βn * c x ^ (n - 1) * deriv_within c s x
@[simp]
theorem
deriv_pow''
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{c : π β π}
{n : β} :
Derivative of x β¦ x^m for m : β€
theorem
has_strict_deriv_at_fpow
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
(m : β€) :
theorem
has_deriv_within_at_fpow
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
(m : β€)
(hx : x β 0)
(s : set π) :
theorem
differentiable_at_fpow
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{m : β€} :
x β 0 β differentiable_at π (Ξ» (x : π), x ^ m) x
theorem
differentiable_within_at_fpow
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{s : set π}
{m : β€} :
x β 0 β differentiable_within_at π (Ξ» (x : π), x ^ m) s x
theorem
differentiable_on_fpow
{π : Type u}
[nondiscrete_normed_field π]
{s : set π}
{m : β€} :
0 β s β differentiable_on π (Ξ» (x : π), x ^ m) s
theorem
deriv_within_fpow
{π : Type u}
[nondiscrete_normed_field π]
{x : π}
{s : set π}
{m : β€} :
unique_diff_within_at π s x β x β 0 β deriv_within (Ξ» (x : π), x ^ m) s x = βm * x ^ (m - 1)
Upper estimates on liminf and limsup
theorem
has_deriv_within_at.limsup_norm_slope_le
{E : Type u}
[normed_group E]
[normed_space β E]
{f : β β E}
{f' : E}
{s : set β}
{x r : β} :
If f has derivative f' within s at x, then for any r > β₯f'β₯ the ratio
β₯f z - f xβ₯ / β₯z - xβ₯ is less than r in some neighborhood of x within s.
In other words, the limit superior of this ratio as z tends to x along s
is less than or equal to β₯f'β₯.
theorem
has_deriv_within_at.limsup_slope_norm_le
{E : Type u}
[normed_group E]
[normed_space β E]
{f : β β E}
{f' : E}
{s : set β}
{x r : β} :
If f has derivative f' within s at x, then for any r > β₯f'β₯ the ratio
(β₯f zβ₯ - β₯f xβ₯) / β₯z - xβ₯ is less than r in some neighborhood of x within s.
In other words, the limit superior of this ratio as z tends to x along s
is less than or equal to β₯f'β₯.
This lemma is a weaker version of has_deriv_within_at.limsup_norm_slope_le
where β₯f zβ₯ - β₯f xβ₯ is replaced by β₯f z - f xβ₯.
theorem
has_deriv_within_at.liminf_right_norm_slope_le
{E : Type u}
[normed_group E]
[normed_space β E]
{f : β β E}
{f' : E}
{x r : β} :
If f has derivative f' within (x, +β) at x, then for any r > β₯f'β₯ the ratio
β₯f z - f xβ₯ / β₯z - xβ₯ is frequently less than r as z β x+0.
In other words, the limit inferior of this ratio as z tends to x+0
is less than or equal to β₯f'β₯. See also has_deriv_within_at.limsup_norm_slope_le
for a stronger version using limit superior and any set s.
theorem
has_deriv_within_at.liminf_right_slope_norm_le
{E : Type u}
[normed_group E]
[normed_space β E]
{f : β β E}
{f' : E}
{x r : β} :
If f has derivative f' within (x, +β) at x, then for any r > β₯f'β₯ the ratio
(β₯f zβ₯ - β₯f xβ₯) / (z - x) is frequently less than r as z β x+0.
In other words, the limit inferior of this ratio as z tends to x+0
is less than or equal to β₯f'β₯.
See also
has_deriv_within_at.limsup_norm_slope_lefor a stronger version using limit superior and any sets;has_deriv_within_at.liminf_right_norm_slope_lefor a stronger version usingβ₯f z - f xβ₯instead ofβ₯f zβ₯ - β₯f xβ₯.