mathlib3 documentation

analysis.calculus.deriv.basic

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:

For the last two notions we also define a functional version:

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:

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
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
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
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
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
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.

Equations
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} :

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} :
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} :

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} :

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} :
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} :
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} :

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} :
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} :
@[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} :
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 : π•œ} :
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 : π•œ} :

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} :

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} :

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) :
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) :
deriv f x = 0
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 π•œ} :
has_deriv_at_filter f f' x L ↔ (Ξ» (x' : π•œ), f x' - f x - (x' - x) β€’ f') =o[L] Ξ» (x' : π•œ), x' - x
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 π•œ} :
has_deriv_at_filter f f' x L ↔ filter.tendsto (Ξ» (x' : π•œ), β€–x' - x‖⁻¹ * β€–f x' - f x - (x' - x) β€’ f'β€–) L (nhds 0)
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 π•œ} :
has_deriv_within_at f f' s x ↔ filter.tendsto (Ξ» (x' : π•œ), β€–x' - x‖⁻¹ * β€–f x' - f x - (x' - x) β€’ f'β€–) (nhds_within x s) (nhds 0)
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 : π•œ} :
has_deriv_at f f' x ↔ (Ξ» (x' : π•œ), f x' - f x - (x' - x) β€’ f') =o[nhds x] Ξ» (x' : π•œ), x' - 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 : π•œ} :
has_deriv_at f f' x ↔ filter.tendsto (Ξ» (x' : π•œ), β€–x' - x‖⁻¹ * β€–f x' - f x - (x' - x) β€’ f'β€–) (nhds x) (nhds 0)
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) :
(Ξ» (x' : π•œ), f x' - f x) =O[L] Ξ» (x' : π•œ), x' - x
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) :
(Ξ» (x' : π•œ), x' - x) =O[L] Ξ» (x' : π•œ), f x' - f x
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) :
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) :
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) :
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) :

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 π•œ} :
@[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 π•œ] :
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 π•œ] :

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 π•œ] :

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 π•œ] :
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 π•œ] :

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 π•œ] :

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) :
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) :

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) :

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 : π•œ} :
has_deriv_at f f' x ↔ (Ξ» (h : π•œ), f (x + h) - f x - h β€’ f') =o[nhds 0] Ξ» (h : π•œ), h
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) :
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) :
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) :
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) :
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) :
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 : π•œ} :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
@[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 : π•œ} :
@[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 π•œ} :
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) :
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) :
deriv f x = f'
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) :
deriv f = f'
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 : π•œ} :
⇑(fderiv π•œ f x) 1 = deriv 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) :
deriv f x = 0
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) :
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) :
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) :
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) :
@[simp]
theorem deriv_within_univ {π•œ : Type u} [nontrivially_normed_field π•œ] {F : Type v} [normed_add_comm_group F] [normed_space π•œ F] {f : π•œ β†’ 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) :
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 : π•œ} :
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 π•œ] :

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) :
deriv f₁ x = deriv f x
@[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 π•œ) :
theorem has_deriv_within_at_id {π•œ : Type u} [nontrivially_normed_field π•œ] (x : π•œ) (s : set π•œ) :
theorem has_deriv_at_id {π•œ : Type u} [nontrivially_normed_field π•œ] (x : π•œ) :
theorem has_deriv_at_id' {π•œ : Type u} [nontrivially_normed_field π•œ] (x : π•œ) :
has_deriv_at (Ξ» (x : π•œ), x) 1 x
theorem has_strict_deriv_at_id {π•œ : Type u} [nontrivially_normed_field π•œ] (x : π•œ) :
theorem deriv_id {π•œ : Type u} [nontrivially_normed_field π•œ] (x : π•œ) :
deriv id x = 1
@[simp]
theorem deriv_id' {π•œ : Type u} [nontrivially_normed_field π•œ] :
deriv id = Ξ» (_x : π•œ), 1
@[simp]
theorem deriv_id'' {π•œ : Type u} [nontrivially_normed_field π•œ] :
deriv (Ξ» (x : π•œ), x) = Ξ» (_x : π•œ), 1
theorem deriv_within_id {π•œ : Type u} [nontrivially_normed_field π•œ] (x : π•œ) (s : set π•œ) (hxs : unique_diff_within_at π•œ s x) :

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) :
deriv (Ξ» (x : π•œ), c) x = 0
@[simp]
theorem deriv_const' {π•œ : Type u} [nontrivially_normed_field π•œ] {F : Type v} [normed_add_comm_group F] [normed_space π•œ F] (c : F) :
deriv (Ξ» (x : π•œ), c) = Ξ» (x : π•œ), 0
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) :
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) :
@[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) :