One-dimensional derivatives #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 (in
linear.lean) - addition (in
add.lean) - sum of finitely many functions (in
add.lean) - negation (in
add.lean) - subtraction (in
add.lean) - star (in
star.lean) - multiplication of two functions in
π β π(inmul.lean) - multiplication of a function in
π β πand of a function inπ β E(inmul.lean) - powers of a function (in
pow.leanandzpow.lean) - inverse
x β xβ»ΒΉ(ininv.lean) - division (in
inv.lean) - composition of a function in
π β Fwith a function inπ β π(incomp.lean) - composition of a function in
F β Ewith a function inπ β F(incomp.lean) - inverse function (assuming that it exists; the inverse function theorem is in
inverse.lean) - polynomials (in
polynomial.lean)
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}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
(f : π β F)
(f' : F)
(x : π)
(L : 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}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
(f : π β F)
(f' : F)
(s : set π)
(x : π) :
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}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
(f : π β F)
(f' : F)
(x : π) :
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}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
(f : π β F)
(f' : F)
(x : π) :
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
noncomputable
def
deriv_within
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
(f : π β F)
(s : set π)
(x : π) :
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
noncomputable
def
deriv
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
(f : π β F)
(x : π) :
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}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_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}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_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}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_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}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_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}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_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}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_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}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_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}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_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}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_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
@[protected]
theorem
has_strict_fderiv_at.has_strict_deriv_at
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_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_deriv_at_iff_has_strict_fderiv_at
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π} :
has_strict_deriv_at f f' x β has_strict_fderiv_at f (1.smul_right f') x
theorem
has_strict_deriv_at.has_strict_fderiv_at
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π} :
has_strict_deriv_at f f' x β has_strict_fderiv_at f (1.smul_right f') x
Alias of the forward direction of has_strict_deriv_at_iff_has_strict_fderiv_at.
theorem
has_deriv_at_iff_has_fderiv_at
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_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
has_deriv_at.has_fderiv_at
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_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
Alias of the forward direction of has_deriv_at_iff_has_fderiv_at.
theorem
deriv_within_zero_of_not_differentiable_within_at
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s : set π}
(h : Β¬differentiable_within_at π f s x) :
deriv_within f s x = 0
theorem
differentiable_within_at_of_deriv_within_ne_zero
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s : set π}
(h : deriv_within f s x β 0) :
differentiable_within_at π f s x
theorem
deriv_zero_of_not_differentiable_at
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{x : π}
(h : Β¬differentiable_at π f x) :
theorem
differentiable_at_of_deriv_ne_zero
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{x : π}
(h : deriv f x β 0) :
differentiable_at π f x
theorem
unique_diff_within_at.eq_deriv
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' fβ' : F}
{x : π}
(s : set π)
(H : unique_diff_within_at π s x)
(h : has_deriv_within_at f f' s x)
(hβ : has_deriv_within_at f fβ' s x) :
f' = fβ'
theorem
has_deriv_at_filter_iff_is_o
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{L : filter π} :
theorem
has_deriv_at_filter_iff_tendsto
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{L : filter π} :
theorem
has_deriv_within_at_iff_is_o
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s : set π} :
has_deriv_within_at f f' s x β (Ξ» (x' : π), f x' - f x - (x' - x) β’ f') =o[nhds_within x s] Ξ» (x' : π), x' - x
theorem
has_deriv_within_at_iff_tendsto
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s : set π} :
theorem
has_deriv_at_iff_is_o
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π} :
theorem
has_deriv_at_iff_tendsto
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π} :
theorem
has_deriv_at_filter.is_O_sub
{π : 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) :
theorem
has_deriv_at_filter.is_O_sub_rev
{π : 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)
(hf' : f' β 0) :
theorem
has_strict_deriv_at.has_deriv_at
{π : 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_deriv_at f f' x
theorem
has_deriv_within_at_congr_set'
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s t : set π}
(y : π)
(h : s =αΆ [nhds_within x {y}αΆ] t) :
has_deriv_within_at f f' s x β has_deriv_within_at f f' t x
theorem
has_deriv_within_at_congr_set
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s t : set π}
(h : s =αΆ [nhds x] t) :
has_deriv_within_at f f' s x β has_deriv_within_at f f' t x
theorem
has_deriv_within_at.congr_set
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s t : set π}
(h : s =αΆ [nhds x] t) :
has_deriv_within_at f f' s x β has_deriv_within_at f f' t x
Alias of the forward direction of has_deriv_within_at_congr_set.
@[simp]
theorem
has_deriv_within_at_diff_singleton
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s : set π} :
has_deriv_within_at f f' (s \ {x}) x β has_deriv_within_at f f' s x
@[simp]
theorem
has_deriv_within_at_Ioi_iff_Ici
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
[partial_order π] :
has_deriv_within_at f f' (set.Ioi x) x β has_deriv_within_at f f' (set.Ici x) x
theorem
has_deriv_within_at.Ioi_of_Ici
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
[partial_order π] :
has_deriv_within_at f f' (set.Ici x) x β has_deriv_within_at f f' (set.Ioi x) x
Alias of the reverse direction of has_deriv_within_at_Ioi_iff_Ici.
theorem
has_deriv_within_at.Ici_of_Ioi
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
[partial_order π] :
has_deriv_within_at f f' (set.Ioi x) x β has_deriv_within_at f f' (set.Ici x) x
Alias of the forward direction of has_deriv_within_at_Ioi_iff_Ici.
@[simp]
theorem
has_deriv_within_at_Iio_iff_Iic
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
[partial_order π] :
has_deriv_within_at f f' (set.Iio x) x β has_deriv_within_at f f' (set.Iic x) x
theorem
has_deriv_within_at.Iic_of_Iio
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
[partial_order π] :
has_deriv_within_at f f' (set.Iio x) x β has_deriv_within_at f f' (set.Iic x) x
Alias of the forward direction of has_deriv_within_at_Iio_iff_Iic.
theorem
has_deriv_within_at.Iio_of_Iic
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
[partial_order π] :
has_deriv_within_at f f' (set.Iic x) x β has_deriv_within_at f f' (set.Iio x) x
Alias of the reverse direction of has_deriv_within_at_Iio_iff_Iic.
theorem
has_deriv_within_at.Ioi_iff_Ioo
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
[linear_order π]
[order_closed_topology π]
{x y : π}
(h : x < y) :
has_deriv_within_at f f' (set.Ioo x y) x β has_deriv_within_at f f' (set.Ioi x) x
theorem
has_deriv_within_at.Ioo_of_Ioi
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
[linear_order π]
[order_closed_topology π]
{x y : π}
(h : x < y) :
has_deriv_within_at f f' (set.Ioi x) x β has_deriv_within_at f f' (set.Ioo x y) x
Alias of the reverse direction of has_deriv_within_at.Ioi_iff_Ioo.
theorem
has_deriv_within_at.Ioi_of_Ioo
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
[linear_order π]
[order_closed_topology π]
{x y : π}
(h : x < y) :
has_deriv_within_at f f' (set.Ioo x y) x β has_deriv_within_at f f' (set.Ioi x) x
Alias of the forward direction of has_deriv_within_at.Ioi_iff_Ioo.
theorem
has_deriv_at_iff_is_o_nhds_zero
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π} :
theorem
has_deriv_at_filter.mono
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{Lβ Lβ : filter π}
(h : has_deriv_at_filter f f' x Lβ)
(hst : Lβ β€ Lβ) :
has_deriv_at_filter f f' x Lβ
theorem
has_deriv_within_at.mono
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s t : set π}
(h : has_deriv_within_at f f' t x)
(hst : s β t) :
has_deriv_within_at f f' s x
theorem
has_deriv_within_at.mono_of_mem
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s t : set π}
(h : has_deriv_within_at f f' t x)
(hst : t β nhds_within x s) :
has_deriv_within_at f f' s x
theorem
has_deriv_at.has_deriv_at_filter
{π : 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 f f' x)
(hL : L β€ nhds x) :
has_deriv_at_filter f f' x L
theorem
has_deriv_at.has_deriv_within_at
{π : 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_at f f' x) :
has_deriv_within_at f f' s x
theorem
has_deriv_within_at.differentiable_within_at
{π : 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) :
differentiable_within_at π f s x
theorem
has_deriv_at.differentiable_at
{π : 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) :
differentiable_at π f x
@[simp]
theorem
has_deriv_within_at_univ
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_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}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{fβ' fβ' : F}
{x : π}
(hβ : has_deriv_at f fβ' x)
(hβ : has_deriv_at f fβ' x) :
fβ' = fβ'
theorem
has_deriv_within_at_inter'
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s t : set π}
(h : 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}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s t : set π}
(h : 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}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s t : set π}
(hs : has_deriv_within_at f f' s x)
(ht : 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}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{s t : set π}
(h : has_deriv_within_at f f' s x)
(ht : s β nhds_within x t) :
has_deriv_within_at f f' t x
theorem
has_deriv_within_at.has_deriv_at
{π : 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)
(hs : s β nhds x) :
has_deriv_at f f' x
theorem
differentiable_within_at.has_deriv_within_at
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s : set π}
(h : 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}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{x : π}
(h : differentiable_at π f x) :
has_deriv_at f (deriv f x) x
@[simp]
theorem
has_deriv_at_deriv_iff
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{x : π} :
has_deriv_at f (deriv f x) x β differentiable_at π f x
@[simp]
theorem
has_deriv_within_at_deriv_within_iff
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s : set π} :
has_deriv_within_at f (deriv_within f s x) s x β differentiable_within_at π f s x
theorem
differentiable_on.has_deriv_at
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s : set π}
(h : differentiable_on π f s)
(hs : s β nhds x) :
has_deriv_at f (deriv f x) x
theorem
has_deriv_at.deriv
{π : 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) :
theorem
deriv_eq
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f f' : π β F}
(h : β (x : π), has_deriv_at f (f' x) x) :
theorem
has_deriv_within_at.deriv_within
{π : 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)
(hxs : unique_diff_within_at π s x) :
deriv_within f s x = f'
theorem
fderiv_within_deriv_within
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_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}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_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}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{x : π} :
theorem
deriv_fderiv
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{x : π} :
1.smul_right (deriv f x) = fderiv π f x
theorem
differentiable_at.deriv_within
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s : set π}
(h : differentiable_at π f x)
(hxs : unique_diff_within_at π s x) :
deriv_within f s x = deriv f x
theorem
has_deriv_within_at.deriv_eq_zero
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s : set π}
(hd : has_deriv_within_at f 0 s x)
(H : unique_diff_within_at π s x) :
theorem
deriv_within_of_mem
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s t : set π}
(st : t β nhds_within x s)
(ht : unique_diff_within_at π s x)
(h : differentiable_within_at π f t x) :
deriv_within f s x = deriv_within f t x
theorem
deriv_within_subset
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s t : set π}
(st : s β t)
(ht : unique_diff_within_at π s x)
(h : differentiable_within_at π f t x) :
deriv_within f s x = deriv_within f t x
theorem
deriv_within_congr_set'
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s t : set π}
(y : π)
(h : s =αΆ [nhds_within x {y}αΆ] t) :
deriv_within f s x = deriv_within f t x
theorem
deriv_within_congr_set
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s t : set π}
(h : s =αΆ [nhds x] t) :
deriv_within f s x = deriv_within f t x
@[simp]
theorem
deriv_within_univ
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F} :
deriv_within f set.univ = deriv f
theorem
deriv_within_inter
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s t : set π}
(ht : t β nhds x) :
deriv_within f (s β© t) x = deriv_within f s x
theorem
deriv_within_of_open
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{x : π}
{s : set π}
(hs : is_open s)
(hx : x β s) :
deriv_within f s x = deriv f x
theorem
deriv_mem_iff
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{s : set F}
{x : π} :
theorem
deriv_within_mem_iff
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{t : set π}
{s : set F}
{x : π} :
deriv_within f t x β s β differentiable_within_at π f t x β§ deriv_within f t x β s β¨ Β¬differentiable_within_at π f t x β§ 0 β s
theorem
differentiable_within_at_Ioi_iff_Ici
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{x : π}
[partial_order π] :
differentiable_within_at π f (set.Ioi x) x β differentiable_within_at π f (set.Ici x) x
theorem
deriv_within_Ioi_eq_Ici
{E : Type u_1}
[normed_add_comm_group E]
[normed_space β E]
(f : β β E)
(x : β) :
deriv_within f (set.Ioi x) x = deriv_within f (set.Ici x) x
Congruence properties of derivatives #
theorem
filter.eventually_eq.has_deriv_at_filter_iff
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{fβ fβ : π β F}
{fβ' fβ' : F}
{x : π}
{L : filter π}
(hβ : fβ =αΆ [L] fβ)
(hx : fβ x = fβ x)
(hβ : 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}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f fβ : π β F}
{f' : F}
{x : π}
{L : filter π}
(h : has_deriv_at_filter f f' x L)
(hL : fβ =αΆ [L] f)
(hx : fβ x = f x) :
has_deriv_at_filter fβ f' x L
theorem
has_deriv_within_at.congr_mono
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f fβ : π β F}
{f' : F}
{x : π}
{s t : set π}
(h : has_deriv_within_at f f' s x)
(ht : β (x : π), x β t β fβ x = f x)
(hx : fβ x = f x)
(hβ : t β s) :
has_deriv_within_at fβ f' t x
theorem
has_deriv_within_at.congr
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f fβ : π β F}
{f' : F}
{x : π}
{s : set π}
(h : has_deriv_within_at f f' s x)
(hs : β (x : π), x β s β fβ x = f x)
(hx : fβ x = f x) :
has_deriv_within_at fβ f' s x
theorem
has_deriv_within_at.congr_of_mem
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f fβ : π β F}
{f' : F}
{x : π}
{s : set π}
(h : has_deriv_within_at f f' s x)
(hs : β (x : π), x β s β fβ x = f x)
(hx : x β s) :
has_deriv_within_at fβ f' s x
theorem
has_deriv_within_at.congr_of_eventually_eq
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f fβ : π β F}
{f' : F}
{x : π}
{s : set π}
(h : has_deriv_within_at f f' s x)
(hβ : fβ =αΆ [nhds_within x s] f)
(hx : fβ x = f x) :
has_deriv_within_at fβ f' s x
theorem
has_deriv_within_at.congr_of_eventually_eq_of_mem
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f fβ : π β F}
{f' : F}
{x : π}
{s : set π}
(h : has_deriv_within_at f f' s x)
(hβ : fβ =αΆ [nhds_within x s] f)
(hx : x β s) :
has_deriv_within_at fβ f' s x
theorem
has_deriv_at.congr_of_eventually_eq
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f fβ : π β F}
{f' : F}
{x : π}
(h : has_deriv_at f f' x)
(hβ : fβ =αΆ [nhds x] f) :
has_deriv_at fβ f' x
theorem
filter.eventually_eq.deriv_within_eq
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f fβ : π β F}
{x : π}
{s : set π}
(hL : fβ =αΆ [nhds_within x s] f)
(hx : fβ x = f x) :
deriv_within fβ s x = deriv_within f s x
theorem
deriv_within_congr
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f fβ : π β F}
{x : π}
{s : set π}
(hs : set.eq_on fβ f s)
(hx : fβ x = f x) :
deriv_within fβ s x = deriv_within f s x
theorem
filter.eventually_eq.deriv_eq
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f fβ : π β F}
{x : π}
(hL : fβ =αΆ [nhds x] f) :
@[protected]
theorem
filter.eventually_eq.deriv
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f fβ : π β F}
{x : π}
(h : fβ =αΆ [nhds x] f) :
Derivative of the identity #
theorem
has_deriv_at_filter_id
{π : Type u}
[nontrivially_normed_field π]
(x : π)
(L : filter π) :
has_deriv_at_filter id 1 x L
theorem
has_deriv_within_at_id
{π : Type u}
[nontrivially_normed_field π]
(x : π)
(s : set π) :
has_deriv_within_at id 1 s x
theorem
has_deriv_at_id
{π : Type u}
[nontrivially_normed_field π]
(x : π) :
has_deriv_at id 1 x
theorem
has_deriv_at_id'
{π : Type u}
[nontrivially_normed_field π]
(x : π) :
has_deriv_at (Ξ» (x : π), x) 1 x
@[simp]
theorem
deriv_within_id
{π : Type u}
[nontrivially_normed_field π]
(x : π)
(s : set π)
(hxs : unique_diff_within_at π s x) :
deriv_within id s x = 1
Derivative of constant functions #
theorem
has_deriv_at_filter_const
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_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}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
(x : π)
(c : F) :
has_strict_deriv_at (Ξ» (x : π), c) 0 x
theorem
has_deriv_within_at_const
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_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}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
(x : π)
(c : F) :
has_deriv_at (Ξ» (x : π), c) 0 x
theorem
deriv_const
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
(x : π)
(c : F) :
@[simp]
theorem
deriv_const'
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
(c : F) :
theorem
deriv_within_const
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
(x : π)
(s : set π)
(c : F)
(hxs : unique_diff_within_at π s x) :
deriv_within (Ξ» (x : π), c) s x = 0
Continuity of a function admitting a derivative #
theorem
has_deriv_at_filter.tendsto_nhds
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{f : π β F}
{f' : F}
{x : π}
{L : filter π}
(hL : L β€ nhds x)
(h : 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}
[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) :
continuous_within_at f s x
theorem
has_deriv_at.continuous_at
{π : 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) :
continuous_at f x
@[protected]
theorem
has_deriv_at.continuous_on
{π : Type u}
[nontrivially_normed_field π]
{F : Type v}
[normed_add_comm_group F]
[normed_space π F]
{s : set π}
{f f' : π β F}
(hderiv : β (x : π), x β s β has_deriv_at f (f' x) x) :
continuous_on f s