mathlib documentation

analysis.calculus.deriv

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:

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} [nondiscrete_normed_field π•œ] {F : Type v} [normed_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} [nondiscrete_normed_field π•œ] {F : Type v} [normed_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} [nondiscrete_normed_field π•œ] {F : Type v} [normed_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} [nondiscrete_normed_field π•œ] {F : Type v} [normed_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
def deriv_within {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_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
def deriv {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_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} [nondiscrete_normed_field π•œ] {F : Type v} [normed_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} [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} :

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

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

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} :
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} :
theorem has_strict_deriv_at_iff_has_strict_fderiv_at {π•œ : 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_strict_fderiv_at {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} :

Alias of has_strict_deriv_at_iff_has_strict_fderiv_at.

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

Expressing has_deriv_at f f' x in terms of has_fderiv_at

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

Alias of has_deriv_at_iff_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 π•œ} (h : Β¬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 : π•œ} (h : Β¬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 π•œ) (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_tendsto {π•œ : 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 (Ξ» (x' : π•œ), βˆ₯x' - xβˆ₯⁻¹ * βˆ₯f x' - f x - (x' - x) β€’ f'βˆ₯) L (𝓝 0)
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 π•œ} :
has_deriv_within_at f f' s x ↔ filter.tendsto (Ξ» (x' : π•œ), βˆ₯x' - xβˆ₯⁻¹ * βˆ₯f x' - f x - (x' - x) β€’ f'βˆ₯) (𝓝[s] x) (𝓝 0)
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 : π•œ} :
has_deriv_at f f' x ↔ filter.tendsto (Ξ» (x' : π•œ), βˆ₯x' - xβˆ₯⁻¹ * βˆ₯f x' - f x - (x' - x) β€’ f'βˆ₯) (𝓝 x) (𝓝 0)
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 : π•œ} (h : has_strict_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 βŠ“ π“Ÿ {x}ᢜ) (𝓝 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)) (𝓝[s \ {x}] x) (𝓝 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 π•œ} (hs : x βˆ‰ s) :
has_deriv_within_at f f' s x ↔ filter.tendsto (Ξ» (y : π•œ), (y - x)⁻¹ β€’ (f y - f x)) (𝓝[s] x) (𝓝 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)) (𝓝[{x}ᢜ] x) (𝓝 f')
theorem has_deriv_within_at_congr_set {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {s t u : set π•œ} (hu : u ∈ 𝓝 x) (h : s ∩ u = t ∩ u) :
theorem has_deriv_within_at.congr_set {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {s t u : set π•œ} (hu : u ∈ 𝓝 x) (h : s ∩ u = t ∩ u) :
has_deriv_within_at f f' s x β†’ has_deriv_within_at f f' t x

Alias of has_deriv_within_at_congr_set.

@[simp]
theorem has_deriv_within_at_diff_singleton {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {s : set π•œ} :
@[simp]
theorem has_deriv_within_at_Ioi_iff_Ici {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} [partial_order π•œ] :
theorem has_deriv_within_at.Ioi_of_Ici {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} [partial_order π•œ] :

Alias of has_deriv_within_at_Ioi_iff_Ici.

theorem has_deriv_within_at.Ici_of_Ioi {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} [partial_order π•œ] :

Alias of has_deriv_within_at_Ioi_iff_Ici.

@[simp]
theorem has_deriv_within_at_Iio_iff_Iic {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} [partial_order π•œ] :
theorem has_deriv_within_at.Iic_of_Iio {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} [partial_order π•œ] :

Alias of has_deriv_within_at_Iio_iff_Iic.

theorem has_deriv_within_at.Iio_of_Iic {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} [partial_order π•œ] :

Alias of has_deriv_within_at_Iio_iff_Iic.

theorem has_deriv_within_at.Ioi_iff_Ioo {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_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} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {f' : F} [linear_order π•œ] [order_closed_topology π•œ] {x y : π•œ} (h : x < y) :

Alias of has_deriv_within_at.Ioi_iff_Ioo.

theorem has_deriv_within_at.Ioi_of_Ioo {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {f' : F} [linear_order π•œ] [order_closed_topology π•œ] {x y : π•œ} (h : x < y) :

Alias of has_deriv_within_at.Ioi_iff_Ioo.

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) (𝓝 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 π•œ} (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} [nondiscrete_normed_field π•œ] {F : Type v} [normed_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_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 π•œ} (h : has_deriv_at f f' x) (hL : L ≀ 𝓝 x) :
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 π•œ} (h : has_deriv_at f f' 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 π•œ} (h : has_deriv_within_at f 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 : π•œ} (h : 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 : π•œ} :
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 : π•œ} (hβ‚€ : has_deriv_at f fβ‚€' x) (h₁ : 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 π•œ} (h : t ∈ 𝓝[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 π•œ} (h : t ∈ 𝓝 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 π•œ} (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} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {s t : set π•œ} (h : has_deriv_within_at f f' s x) (ht : s ∈ 𝓝[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 π•œ} (h : has_deriv_within_at f f' s x) (hs : s ∈ 𝓝 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 π•œ} (h : differentiable_within_at π•œ f 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 : π•œ} (h : differentiable_at π•œ f x) :
theorem differentiable_on.has_deriv_at {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {x : π•œ} {s : set π•œ} (h : differentiable_on π•œ f s) (hs : s ∈ 𝓝 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 : π•œ} (h : 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 π•œ} (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} [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 : π•œ} :
⇑(fderiv π•œ f x) 1 = deriv 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 π•œ} (h : differentiable_at π•œ f x) (hxs : 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 π•œ} (st : s βŠ† t) (ht : unique_diff_within_at π•œ s x) (h : differentiable_within_at π•œ f t x) :
@[simp]
theorem deriv_within_univ {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ 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 π•œ} (ht : t ∈ 𝓝 x) (hs : unique_diff_within_at π•œ s x) :
theorem deriv_within_of_open {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_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

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 π•œ} (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} [nondiscrete_normed_field π•œ] {F : Type v} [normed_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} [nondiscrete_normed_field π•œ] {F : Type v} [normed_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} [nondiscrete_normed_field π•œ] {F : Type v} [normed_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_eventually_eq {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f f₁ : π•œ β†’ F} {f' : F} {x : π•œ} {s : set π•œ} (h : has_deriv_within_at f f' s x) (h₁ : f₁ =αΆ [𝓝[s] x] 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} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f f₁ : π•œ β†’ F} {f' : F} {x : π•œ} {s : set π•œ} (h : has_deriv_within_at f f' s x) (h₁ : f₁ =αΆ [𝓝[s] x] f) (hx : x ∈ s) :
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 : π•œ} (h : has_deriv_at f f' x) (h₁ : f₁ =αΆ [𝓝 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 π•œ} (hs : unique_diff_within_at π•œ s x) (hL : f₁ =αΆ [𝓝[s] x] f) (hx : 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 π•œ} (hs : unique_diff_within_at π•œ s x) (hL : βˆ€ (y : π•œ), y ∈ s β†’ f₁ y = f y) (hx : 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 : π•œ} (hL : f₁ =αΆ [𝓝 x] f) :
deriv f₁ x = deriv f x
theorem filter.eventually_eq.deriv {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f f₁ : π•œ β†’ F} {x : π•œ} (h : f₁ =αΆ [𝓝 x] f) :

Derivative of the identity #

theorem has_deriv_at_filter_id {π•œ : Type u} [nondiscrete_normed_field π•œ] (x : π•œ) (L : filter π•œ) :
theorem has_deriv_within_at_id {π•œ : Type u} [nondiscrete_normed_field π•œ] (x : π•œ) (s : set π•œ) :
theorem has_deriv_at_id {π•œ : Type u} [nondiscrete_normed_field π•œ] (x : π•œ) :
theorem has_deriv_at_id' {π•œ : Type u} [nondiscrete_normed_field π•œ] (x : π•œ) :
has_deriv_at (Ξ» (x : π•œ), x) 1 x
theorem has_strict_deriv_at_id {π•œ : Type u} [nondiscrete_normed_field π•œ] (x : π•œ) :
theorem deriv_id {π•œ : Type u} [nondiscrete_normed_field π•œ] (x : π•œ) :
deriv id x = 1
@[simp]
theorem deriv_id' {π•œ : Type u} [nondiscrete_normed_field π•œ] :
deriv id = Ξ» (_x : π•œ), 1
@[simp]
theorem deriv_id'' {π•œ : Type u} [nondiscrete_normed_field π•œ] :
deriv (Ξ» (x : π•œ), x) = Ξ» (_x : π•œ), 1
theorem deriv_within_id {π•œ : Type u} [nondiscrete_normed_field π•œ] (x : π•œ) (s : set π•œ) (hxs : unique_diff_within_at π•œ s x) :

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

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) :
theorem linear_map.has_strict_deriv_at {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {x : π•œ} (e : π•œ β†’β‚—[π•œ] F) :
theorem linear_map.has_deriv_at {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {x : π•œ} (e : π•œ β†’β‚—[π•œ] F) :
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) :
@[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) (hxs : unique_diff_within_at π•œ s x) :

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 π•œ} (hf : has_deriv_at_filter f f' x L) (hg : has_deriv_at_filter g g' x L) :
has_deriv_at_filter (Ξ» (y : π•œ), f y + g y) (f' + g') x L
theorem has_strict_deriv_at.add {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f g : π•œ β†’ F} {f' g' : F} {x : π•œ} (hf : has_strict_deriv_at f f' x) (hg : has_strict_deriv_at g g' x) :
has_strict_deriv_at (Ξ» (y : π•œ), f y + g y) (f' + g') x
theorem has_deriv_within_at.add {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f g : π•œ β†’ F} {f' g' : F} {x : π•œ} {s : set π•œ} (hf : has_deriv_within_at f f' s x) (hg : has_deriv_within_at g g' s x) :
has_deriv_within_at (Ξ» (y : π•œ), f y + g y) (f' + g') s x
theorem has_deriv_at.add {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f g : π•œ β†’ F} {f' g' : F} {x : π•œ} (hf : has_deriv_at f f' x) (hg : has_deriv_at g g' x) :
has_deriv_at (Ξ» (x : π•œ), f x + g x) (f' + g') x
theorem deriv_within_add {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f g : π•œ β†’ F} {x : π•œ} {s : set π•œ} (hxs : unique_diff_within_at π•œ s x) (hf : differentiable_within_at π•œ f s x) (hg : differentiable_within_at π•œ g s x) :
deriv_within (Ξ» (y : π•œ), f y + g y) s x = deriv_within f s x + deriv_within g s x
@[simp]
theorem deriv_add {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f g : π•œ β†’ F} {x : π•œ} (hf : differentiable_at π•œ f x) (hg : 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) (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 : π•œ} (c : F) :
deriv (Ξ» (y : π•œ), f y + c) x = deriv f x
@[simp]
theorem deriv_add_const' {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} (c : F) :
deriv (Ξ» (y : π•œ), f y + c) = deriv 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) (hf : has_deriv_at_filter f f' x L) :
has_deriv_at_filter (Ξ» (y : π•œ), c + f y) f' x L
theorem has_deriv_within_at.const_add {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {s : set π•œ} (c : F) (hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (Ξ» (y : π•œ), c + f y) f' s x
theorem has_deriv_at.const_add {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} (c : F) (hf : has_deriv_at f f' x) :
has_deriv_at (Ξ» (x : π•œ), c + f x) f' x
theorem deriv_within_const_add {π•œ : Type u} [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) :
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) :
deriv (Ξ» (y : π•œ), c + f y) x = deriv f x
@[simp]
theorem deriv_const_add' {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} (c : F) :
deriv (Ξ» (y : π•œ), c + f y) = deriv f

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} (h : βˆ€ (i : ΞΉ), i ∈ u β†’ has_deriv_at_filter (A i) (A' i) x L) :
has_deriv_at_filter (Ξ» (y : π•œ), βˆ‘ (i : ΞΉ) in u, A i y) (βˆ‘ (i : ΞΉ) in u, 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} (h : βˆ€ (i : ΞΉ), i ∈ u β†’ has_strict_deriv_at (A i) (A' i) x) :
has_strict_deriv_at (Ξ» (y : π•œ), βˆ‘ (i : ΞΉ) in u, A i y) (βˆ‘ (i : ΞΉ) in u, 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} (h : βˆ€ (i : ΞΉ), i ∈ u β†’ has_deriv_within_at (A i) (A' i) s x) :
has_deriv_within_at (Ξ» (y : π•œ), βˆ‘ (i : ΞΉ) in u, A i y) (βˆ‘ (i : ΞΉ) in u, 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} (h : βˆ€ (i : ΞΉ), i ∈ u β†’ has_deriv_at (A i) (A' i) x) :
has_deriv_at (Ξ» (y : π•œ), βˆ‘ (i : ΞΉ) in u, A i y) (βˆ‘ (i : ΞΉ) in u, 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} (hxs : unique_diff_within_at π•œ s x) (h : βˆ€ (i : ΞΉ), i ∈ u β†’ differentiable_within_at π•œ (A i) s x) :
deriv_within (Ξ» (y : π•œ), βˆ‘ (i : ΞΉ) in u, A i y) s x = βˆ‘ (i : ΞΉ) in u, 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} (h : βˆ€ (i : ΞΉ), i ∈ u β†’ differentiable_at π•œ (A i) x) :
deriv (Ξ» (y : π•œ), βˆ‘ (i : ΞΉ) in u, A i y) x = βˆ‘ (i : ΞΉ) in u, deriv (A i) x

Derivatives of functions f : π•œ β†’ Ξ  i, E i #

@[simp]
theorem has_strict_deriv_at_pi {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} {ΞΉ : Type u_1} [fintype ΞΉ] {E' : ΞΉ β†’ Type u_2} [Ξ  (i : ΞΉ), normed_group (E' i)] [Ξ  (i : ΞΉ), normed_space π•œ (E' i)] {Ο† : π•œ β†’ Ξ  (i : ΞΉ), E' i} {Ο†' : Ξ  (i : ΞΉ), E' i} :
has_strict_deriv_at Ο† Ο†' x ↔ βˆ€ (i : ΞΉ), has_strict_deriv_at (Ξ» (x : π•œ), Ο† x i) (Ο†' i) x
@[simp]
theorem has_deriv_at_filter_pi {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} {L : filter π•œ} {ΞΉ : Type u_1} [fintype ΞΉ] {E' : ΞΉ β†’ Type u_2} [Ξ  (i : ΞΉ), normed_group (E' i)] [Ξ  (i : ΞΉ), normed_space π•œ (E' i)] {Ο† : π•œ β†’ Ξ  (i : ΞΉ), E' i} {Ο†' : Ξ  (i : ΞΉ), E' i} :
has_deriv_at_filter Ο† Ο†' x L ↔ βˆ€ (i : ΞΉ), has_deriv_at_filter (Ξ» (x : π•œ), Ο† x i) (Ο†' i) x L
theorem has_deriv_at_pi {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} {ΞΉ : Type u_1} [fintype ΞΉ] {E' : ΞΉ β†’ Type u_2} [Ξ  (i : ΞΉ), normed_group (E' i)] [Ξ  (i : ΞΉ), normed_space π•œ (E' i)] {Ο† : π•œ β†’ Ξ  (i : ΞΉ), E' i} {Ο†' : Ξ  (i : ΞΉ), E' i} :
has_deriv_at Ο† Ο†' x ↔ βˆ€ (i : ΞΉ), has_deriv_at (Ξ» (x : π•œ), Ο† x i) (Ο†' i) x
theorem has_deriv_within_at_pi {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} {s : set π•œ} {ΞΉ : Type u_1} [fintype ΞΉ] {E' : ΞΉ β†’ Type u_2} [Ξ  (i : ΞΉ), normed_group (E' i)] [Ξ  (i : ΞΉ), normed_space π•œ (E' i)] {Ο† : π•œ β†’ Ξ  (i : ΞΉ), E' i} {Ο†' : Ξ  (i : ΞΉ), E' i} :
has_deriv_within_at Ο† Ο†' s x ↔ βˆ€ (i : ΞΉ), has_deriv_within_at (Ξ» (x : π•œ), Ο† x i) (Ο†' i) s x
theorem deriv_within_pi {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} {s : set π•œ} {ΞΉ : Type u_1} [fintype ΞΉ] {E' : ΞΉ β†’ Type u_2} [Ξ  (i : ΞΉ), normed_group (E' i)] [Ξ  (i : ΞΉ), normed_space π•œ (E' i)] {Ο† : π•œ β†’ Ξ  (i : ΞΉ), E' i} (h : βˆ€ (i : ΞΉ), differentiable_within_at π•œ (Ξ» (x : π•œ), Ο† x i) s x) (hs : unique_diff_within_at π•œ s x) :
deriv_within Ο† s x = Ξ» (i : ΞΉ), deriv_within (Ξ» (x : π•œ), Ο† x i) s x
theorem deriv_pi {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} {ΞΉ : Type u_1} [fintype ΞΉ] {E' : ΞΉ β†’ Type u_2} [Ξ  (i : ΞΉ), normed_group (E' i)] [Ξ  (i : ΞΉ), normed_space π•œ (E' i)] {Ο† : π•œ β†’ Ξ  (i : ΞΉ), E' i} (h : βˆ€ (i : ΞΉ), differentiable_at π•œ (Ξ» (x : π•œ), Ο† x i) x) :
deriv Ο† x = Ξ» (i : ΞΉ), deriv (Ξ» (x : π•œ), Ο† x i) x

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' : π•œ} (hc : has_deriv_within_at c c' s x) (hf : 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' : π•œ} (hc : has_deriv_at c c' x) (hf : 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' : π•œ} (hc : has_strict_deriv_at c c' x) (hf : 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 : π•œ β†’ π•œ} (hxs : unique_diff_within_at π•œ s x) (hc : differentiable_within_at π•œ c s x) (hf : 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 : π•œ β†’ π•œ} (hc : differentiable_at π•œ c x) (hf : 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) :
deriv (Ξ» (y : π•œ), c y β€’ f) x = deriv c x β€’ 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 : π•œ) (hf : 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 : π•œ) (hf : 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 : π•œ) (hf : 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 : π•œ) (hf : differentiable_at π•œ f x) :
deriv (Ξ» (y : π•œ), c β€’ f y) x = c β€’ deriv f x

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 π•œ} (h : has_deriv_at_filter f f' x L) :
has_deriv_at_filter (Ξ» (x : π•œ), -f x) (-f') x L
theorem has_deriv_within_at.neg {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {s : set π•œ} (h : has_deriv_within_at f f' s x) :
has_deriv_within_at (Ξ» (x : π•œ), -f x) (-f') s x
theorem has_deriv_at.neg {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} (h : has_deriv_at f f' x) :
has_deriv_at (Ξ» (x : π•œ), -f x) (-f') x
theorem has_strict_deriv_at.neg {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} (h : has_strict_deriv_at f f' x) :
has_strict_deriv_at (Ξ» (x : π•œ), -f x) (-f') x
theorem deriv_within.neg {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {x : π•œ} {s : set π•œ} (hxs : unique_diff_within_at π•œ s x) :
deriv_within (Ξ» (y : π•œ), -f y) s x = -deriv_within f s x
theorem deriv.neg {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {x : π•œ} :
deriv (Ξ» (y : π•œ), -f y) x = -deriv f x
@[simp]
theorem deriv.neg' {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} :
deriv (Ξ» (y : π•œ), -f y) = Ξ» (x : π•œ), -deriv f x

Derivative of the negation function (i.e has_neg.neg) #

theorem has_deriv_at_filter_neg {π•œ : Type u} [nondiscrete_normed_field π•œ] (x : π•œ) (L : filter π•œ) :
theorem has_deriv_within_at_neg {π•œ : Type u} [nondiscrete_normed_field π•œ] (x : π•œ) (s : set π•œ) :
theorem has_deriv_at_neg {π•œ : Type u} [nondiscrete_normed_field π•œ] (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 : π•œ) :
theorem deriv_neg {π•œ : Type u} [nondiscrete_normed_field π•œ] (x : π•œ) :
@[simp]
theorem deriv_neg' {π•œ : Type u} [nondiscrete_normed_field π•œ] :
deriv has_neg.neg = Ξ» (_x : π•œ), -1
@[simp]
theorem deriv_neg'' {π•œ : Type u} [nondiscrete_normed_field π•œ] (x : π•œ) :
deriv (Ξ» (x : π•œ), -x) x = -1
theorem deriv_within_neg {π•œ : Type u} [nondiscrete_normed_field π•œ] (x : π•œ) (s : set π•œ) (hxs : unique_diff_within_at π•œ s x) :
theorem differentiable_neg {π•œ : Type u} [nondiscrete_normed_field π•œ] :
theorem differentiable_on_neg {π•œ : Type u} [nondiscrete_normed_field π•œ] (s : set π•œ) :

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 π•œ} (hf : has_deriv_at_filter f f' x L) (hg : has_deriv_at_filter g g' x L) :
has_deriv_at_filter (Ξ» (x : π•œ), f x - g x) (f' - g') x L
theorem has_deriv_within_at.sub {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f g : π•œ β†’ F} {f' g' : F} {x : π•œ} {s : set π•œ} (hf : has_deriv_within_at f f' s x) (hg : has_deriv_within_at g g' s x) :
has_deriv_within_at (Ξ» (x : π•œ), f x - g x) (f' - g') s x
theorem has_deriv_at.sub {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f g : π•œ β†’ F} {f' g' : F} {x : π•œ} (hf : has_deriv_at f f' x) (hg : has_deriv_at g g' x) :
has_deriv_at (Ξ» (x : π•œ), f x - g x) (f' - g') x
theorem has_strict_deriv_at.sub {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f g : π•œ β†’ F} {f' g' : F} {x : π•œ} (hf : has_strict_deriv_at f f' x) (hg : has_strict_deriv_at g g' x) :
has_strict_deriv_at (Ξ» (x : π•œ), f x - g x) (f' - g') x
theorem deriv_within_sub {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f g : π•œ β†’ F} {x : π•œ} {s : set π•œ} (hxs : unique_diff_within_at π•œ s x) (hf : differentiable_within_at π•œ f s x) (hg : differentiable_within_at π•œ g s x) :
deriv_within (Ξ» (y : π•œ), f y - g y) s x = deriv_within f s x - deriv_within g s x
@[simp]
theorem deriv_sub {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f g : π•œ β†’ F} {x : π•œ} (hf : differentiable_at π•œ f x) (hg : 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 π•œ} (h : 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) (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) :
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) (hf : has_deriv_at_filter f f' x L) :
has_deriv_at_filter (Ξ» (x : π•œ), c - f x) (-f') x L
theorem has_deriv_within_at.const_sub {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {s : set π•œ} (c : F) (hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (Ξ» (x : π•œ), c - f x) (-f') s x
theorem has_strict_deriv_at.const_sub {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} (c : F) (hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (Ξ» (x : π•œ), c - f x) (-f') x
theorem has_deriv_at.const_sub {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} (c : F) (hf : has_deriv_at f f' x) :
has_deriv_at (Ξ» (x : π•œ), c - f x) (-f') x
theorem deriv_within_const_sub {π•œ : Type u} [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) :
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) :
deriv (Ξ» (y : π•œ), c - f y) x = -deriv f x

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 π•œ} (hL : L ≀ 𝓝 x) (h : has_deriv_at_filter f f' x L) :
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 π•œ} (h : has_deriv_within_at f 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 : π•œ} (h : has_deriv_at f f' x) :
theorem has_deriv_at.continuous_on {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {s : set π•œ} {f f' : π•œ β†’ F} (hderiv : βˆ€ (x : π•œ), x ∈ s β†’ has_deriv_at f (f' x) 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} (hf₁ : has_deriv_at_filter f₁ f₁' x L) (hfβ‚‚ : 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} (hf₁ : has_deriv_within_at f₁ f₁' s x) (hfβ‚‚ : 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} (hf₁ : has_deriv_at f₁ f₁' x) (hfβ‚‚ : has_deriv_at fβ‚‚ fβ‚‚' x) :
has_deriv_at (Ξ» (x : π•œ), (f₁ x, fβ‚‚ x)) (f₁', fβ‚‚') x
theorem has_strict_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} (hf₁ : has_strict_deriv_at f₁ f₁' x) (hfβ‚‚ : has_strict_deriv_at fβ‚‚ fβ‚‚' x) :
has_strict_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' : π•œ} (hg : has_deriv_at_filter g g' (h x) (filter.map h L)) (hh : has_deriv_at_filter h h' 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 π•œ} (hg : has_deriv_within_at g g' t (h x)) (hh : has_deriv_within_at h h' s x) (hst : s βŠ† h ⁻¹' t) :
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' : π•œ} (hg : has_deriv_at g g' (h x)) (hh : 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' : π•œ} (hg : has_strict_deriv_at g g' (h x)) (hh : has_strict_deriv_at h h' 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' : π•œ} (hg : has_deriv_at g g' (h x)) (hh : has_deriv_within_at h h' 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 : π•œ β†’ π•œ} (hg : differentiable_within_at π•œ g t (h x)) (hh : differentiable_within_at π•œ h s x) (hs : s βŠ† h ⁻¹' t) (hxs : unique_diff_within_at π•œ s x) :
theorem deriv.scomp {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {g : π•œ β†’ F} (x : π•œ) {h : π•œ β†’ π•œ} (hg : differentiable_at π•œ g (h x)) (hh : differentiable_at π•œ h x) :
deriv (g ∘ h) x = deriv h x β€’ deriv g (h x)

Derivative of the composition of a scalar and vector functions #

theorem has_deriv_at_filter.comp_has_fderiv_at_filter {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type w} [normed_group E] [normed_space π•œ E] {h₁ : π•œ β†’ π•œ} {h₁' : π•œ} {f : E β†’ π•œ} {f' : E β†’L[π•œ] π•œ} (x : E) {L : filter E} (hh₁ : has_deriv_at_filter h₁ h₁' (f x) (filter.map f L)) (hf : has_fderiv_at_filter f f' x L) :
has_fderiv_at_filter (h₁ ∘ f) (h₁' β€’ f') x L
theorem has_strict_deriv_at.comp_has_strict_fderiv_at {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type w} [normed_group E] [normed_space π•œ E] {h₁ : π•œ β†’ π•œ} {h₁' : π•œ} {f : E β†’ π•œ} {f' : E β†’L[π•œ] π•œ} (x : E) (hh₁ : has_strict_deriv_at h₁ h₁' (f x)) (hf : has_strict_fderiv_at f f' x) :
has_strict_fderiv_at (h₁ ∘ f) (h₁' β€’ f') x
theorem has_deriv_at.comp_has_fderiv_at {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type w} [normed_group E] [normed_space π•œ E] {h₁ : π•œ β†’ π•œ} {h₁' : π•œ} {f : E β†’ π•œ} {f' : E β†’L[π•œ] π•œ} (x : E) (hh₁ : has_deriv_at h₁ h₁' (f x)) (hf : has_fderiv_at f f' x) :
has_fderiv_at (h₁ ∘ f) (h₁' β€’ f') x
theorem has_deriv_at.comp_has_fderiv_within_at {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type w} [normed_group E] [normed_space π•œ E] {h₁ : π•œ β†’ π•œ} {h₁' : π•œ} {f : E β†’ π•œ} {f' : E β†’L[π•œ] π•œ} {s : set E} (x : E) (hh₁ : has_deriv_at h₁ h₁' (f x)) (hf : has_fderiv_within_at f f' s x) :
has_fderiv_within_at (h₁ ∘ f) (h₁' β€’ f') s x
theorem has_deriv_within_at.comp_has_fderiv_within_at {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type w} [normed_group E] [normed_space π•œ E] {h₁ : π•œ β†’ π•œ} {h₁' : π•œ} {f : E β†’ π•œ} {f' : E β†’L[π•œ] π•œ} {s : set E} {t : set π•œ} (x : E) (hh₁ : has_deriv_within_at h₁ h₁' t (f x)) (hf : has_fderiv_within_at f f' s x) (hst : set.maps_to f s t) :
has_fderiv_within_at (h₁ ∘ f) (h₁' β€’ f') s 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β‚‚' : π•œ} (hh₁ : has_deriv_at_filter h₁ h₁' (hβ‚‚ x) (filter.map hβ‚‚ L)) (hhβ‚‚ : 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 π•œ} (hh₁ : has_deriv_within_at h₁ h₁' t (hβ‚‚ x)) (hhβ‚‚ : has_deriv_within_at hβ‚‚ hβ‚‚' s x) (hst : 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β‚‚' : π•œ} (hh₁ : has_deriv_at h₁ h₁' (hβ‚‚ x)) (hhβ‚‚ : 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β‚‚' : π•œ} (hh₁ : has_strict_deriv_at h₁ h₁' (hβ‚‚ x)) (hhβ‚‚ : 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β‚‚' : π•œ} (hh₁ : has_deriv_at h₁ h₁' (hβ‚‚ x)) (hhβ‚‚ : 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β‚‚ : π•œ β†’ π•œ} (hh₁ : differentiable_within_at π•œ h₁ t (hβ‚‚ x)) (hhβ‚‚ : differentiable_within_at π•œ hβ‚‚ s x) (hs : s βŠ† hβ‚‚ ⁻¹' t) (hxs : 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β‚‚ : π•œ β†’ π•œ} (hh₁ : differentiable_at π•œ h₁ (hβ‚‚ x)) (hhβ‚‚ : 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 : β„•) :
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 : β„•) :
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 : β„•) :

Derivative of the composition of a function between vector spaces and a function 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} (hl : has_fderiv_within_at l l' t (f x)) (hf : has_deriv_within_at f f' s x) (hst : set.maps_to f s t) :

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_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} (hl : has_fderiv_at l l' (f x)) (hf : has_deriv_within_at f f' s x) :
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} (hl : has_fderiv_at l l' (f x)) (hf : 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_strict_fderiv_at.comp_has_strict_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} (hl : has_strict_fderiv_at l l' (f x)) (hf : has_strict_deriv_at f f' 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} (hl : differentiable_within_at π•œ l t (f x)) (hf : differentiable_within_at π•œ f s x) (hs : set.maps_to f s t) (hxs : 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} (hl : differentiable_at π•œ l (f x)) (hf : differentiable_at π•œ f x) :
deriv (l ∘ f) x = ⇑(fderiv π•œ l (f x)) (deriv f x)

Derivative of the multiplication of two functions #

theorem has_deriv_within_at.mul {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} {s : set π•œ} {𝔸 : Type u_2} [normed_ring 𝔸] [normed_algebra π•œ 𝔸] {c d : π•œ β†’ 𝔸} {c' d' : 𝔸} (hc : has_deriv_within_at c c' s x) (hd : 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 : π•œ} {𝔸 : Type u_2} [normed_ring 𝔸] [normed_algebra π•œ 𝔸] {c d : π•œ β†’ 𝔸} {c' d' : 𝔸} (hc : has_deriv_at c c' x) (hd : 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 : π•œ} {𝔸 : Type u_2} [normed_ring 𝔸] [normed_algebra π•œ 𝔸] {c d : π•œ β†’ 𝔸} {c' d' : 𝔸} (hc : has_strict_deriv_at c c' x) (hd : 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 π•œ} {𝔸 : Type u_2} [normed_ring 𝔸] [normed_algebra π•œ 𝔸] {c d : π•œ β†’ 𝔸} (hxs : unique_diff_within_at π•œ s x) (hc : differentiable_within_at π•œ c s x) (hd : 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 : π•œ} {𝔸 : Type u_2} [normed_ring 𝔸] [normed_algebra π•œ 𝔸] {c d : π•œ β†’ 𝔸} (hc : differentiable_at π•œ c x) (hd : 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 π•œ} {𝔸 : Type u_2} [normed_ring 𝔸] [normed_algebra π•œ 𝔸] {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 : π•œ} {𝔸 : Type u_2} [normed_ring 𝔸] [normed_algebra π•œ 𝔸] {c : π•œ β†’ 𝔸} {c' : 𝔸} (hc : has_deriv_at c c' x) (d : 𝔸) :
has_deriv_at (Ξ» (y : π•œ), (c y) * d) (c' * d) x
theorem has_strict_deriv_at.mul_const {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} {𝔸 : Type u_2} [normed_ring 𝔸] [normed_algebra π•œ 𝔸] {c : π•œ β†’ 𝔸} {c' : 𝔸} (hc : has_strict_deriv_at c c' x) (d : 𝔸) :
has_strict_deriv_at (Ξ» (y : π•œ), (c y) * d) (c' * d) x
theorem deriv_within_mul_const {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} {s : set π•œ} {𝔸 : Type u_2} [normed_ring 𝔸] [normed_algebra π•œ 𝔸] {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 : π•œ} {𝔸 : Type u_2} [normed_ring 𝔸] [normed_algebra π•œ 𝔸] {c : π•œ β†’ 𝔸} (hc : differentiable_at π•œ c x) (d : 𝔸) :
deriv (Ξ» (y : π•œ), (c y) * d) x = (deriv c x) * d
theorem deriv_mul_const_field {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} {π•œ' : Type u_1} [normed_field π•œ'] [normed_algebra π•œ π•œ'] {u : π•œ β†’ π•œ'} (v : π•œ') :
deriv (Ξ» (y : π•œ), (u y) * v) x = (deriv u x) * v
@[simp]
theorem deriv_mul_const_field' {π•œ : Type u} [nondiscrete_normed_field π•œ] {π•œ' : Type u_1} [normed_field π•œ'] [normed_algebra π•œ π•œ'] {u : π•œ β†’ π•œ'} (v : π•œ') :
deriv (Ξ» (x : π•œ), (u x) * v) = Ξ» (x : π•œ), (deriv u x) * v
theorem has_deriv_within_at.const_mul {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} {s : set π•œ} {𝔸 : Type u_2} [normed_ring 𝔸] [normed_algebra π•œ 𝔸] {d : π•œ β†’ 𝔸} {d' : 𝔸} (c : 𝔸) (hd : 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 : π•œ} {𝔸 : Type u_2} [normed_ring 𝔸] [normed_algebra π•œ 𝔸] {d : π•œ β†’ 𝔸} {d' : 𝔸} (c : 𝔸) (hd : has_deriv_at d d' x) :
has_deriv_at (Ξ» (y : π•œ), c * d y) (c * d') x
theorem has_strict_deriv_at.const_mul {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} {𝔸 : Type u_2} [normed_ring 𝔸] [normed_algebra π•œ 𝔸] {d : π•œ β†’ 𝔸} {d' : 𝔸} (c : 𝔸) (hd : has_strict_deriv_at d d' x) :
has_strict_deriv_at (Ξ» (y : π•œ), c * d y) (c * d') x
theorem deriv_within_const_mul {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} {s : set π•œ} {𝔸 : Type u_2} [normed_ring 𝔸] [normed_algebra π•œ 𝔸] {d : π•œ β†’ 𝔸} (hxs : unique_diff_within_at π•œ s x) (c : 𝔸) (hd : 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 : π•œ} {𝔸 : Type u_2} [normed_ring 𝔸] [normed_algebra π•œ 𝔸] {d : π•œ β†’ 𝔸} (c : 𝔸) (hd : differentiable_at π•œ d x) :
deriv (Ξ» (y : π•œ), c * d y) x = c * deriv d x
theorem deriv_const_mul_field {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} {π•œ' : Type u_1} [normed_field π•œ'] [normed_algebra π•œ π•œ'] {v : π•œ β†’ π•œ'} (u : π•œ') :
deriv (Ξ» (y : π•œ), u * v y) x = u * deriv v x
@[simp]
theorem deriv_const_mul_field' {π•œ : Type u} [nondiscrete_normed_field π•œ] {π•œ' : Type u_1} [normed_field π•œ'] [normed_algebra π•œ π•œ'] {v : π•œ β†’ π•œ'} (u : π•œ') :
deriv (Ξ» (x : π•œ), u * v x) = Ξ» (x : π•œ), u * deriv v x

Derivative of x ↦ x⁻¹ #

theorem has_strict_deriv_at_inv {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} (hx : x β‰  0) :
theorem has_deriv_at_inv {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} (x_ne_zero : x β‰  0) :
has_deriv_at (Ξ» (y : π•œ), y⁻¹) (-(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 : π•œ} :
differentiable_at π•œ (Ξ» (x : π•œ), x⁻¹) x ↔ x β‰  0
theorem differentiable_within_at_inv {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} {s : set π•œ} (x_ne_zero : 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_inv {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} :
deriv (Ξ» (x : π•œ), x⁻¹) x = -(x ^ 2)⁻¹
@[simp]
theorem deriv_inv' {π•œ : Type u} [nondiscrete_normed_field π•œ] :
deriv (Ξ» (x : π•œ), x⁻¹) = Ξ» (x : π•œ), -(x ^ 2)⁻¹
theorem deriv_within_inv {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} {s : set π•œ} (x_ne_zero : x β‰  0) (hxs : 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_ne_zero : 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_ne_zero : x β‰  0) :
has_fderiv_within_at (Ξ» (x : π•œ), x⁻¹) (1.smul_right (-(x ^ 2)⁻¹)) s x
theorem fderiv_inv {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} :
fderiv π•œ (Ξ» (x : π•œ), x⁻¹) x = 1.smul_right (-(x ^ 2)⁻¹)
theorem fderiv_within_inv {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} {s : set π•œ} (x_ne_zero : x β‰  0) (hxs : 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' : π•œ} (hc : has_deriv_within_at c c' s x) (hx : 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' : π•œ} (hc : has_deriv_at c c' x) (hx : 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 : π•œ β†’ π•œ} (hc : differentiable_within_at π•œ c s x) (hx : c x β‰  0) :
differentiable_within_at π•œ (Ξ» (x : π•œ), (c x)⁻¹) s x
@[simp]
theorem differentiable_at.inv {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} {c : π•œ β†’ π•œ} (hc : differentiable_at π•œ c x) (hx : c x β‰  0) :
differentiable_at π•œ (Ξ» (x : π•œ), (c x)⁻¹) x
theorem differentiable_on.inv {π•œ : Type u} [nondiscrete_normed_field π•œ] {s : set π•œ} {c : π•œ β†’ π•œ} (hc : differentiable_on π•œ c s) (hx : βˆ€ (x : π•œ), x ∈ s β†’ c x β‰  0) :
differentiable_on π•œ (Ξ» (x : π•œ), (c x)⁻¹) s
@[simp]
theorem differentiable.inv {π•œ : Type u} [nondiscrete_normed_field π•œ] {c : π•œ β†’ π•œ} (hc : differentiable π•œ c) (hx : βˆ€ (x : π•œ), c x β‰  0) :
differentiable π•œ (Ξ» (x : π•œ), (c x)⁻¹)
theorem deriv_within_inv' {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} {s : set π•œ} {c : π•œ β†’ π•œ} (hc : differentiable_within_at π•œ c s x) (hx : c x β‰  0) (hxs : unique_diff_within_at π•œ s x) :
deriv_within (Ξ» (x : π•œ), (c x)⁻¹) s x = -deriv_within c s x / c x ^ 2
@[simp]
theorem deriv_inv'' {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} {c : π•œ β†’ π•œ} (hc : differentiable_at π•œ c x) (hx : c x β‰  0) :
deriv (Ξ» (x : π•œ), (c x)⁻¹) x = -deriv c x / c x ^ 2

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' : π•œ} (hc : has_deriv_within_at c c' s x) (hd : has_deriv_within_at d d' s x) (hx : 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_strict_deriv_at.div {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} {c d : π•œ β†’ π•œ} {c' d' : π•œ} (hc : has_strict_deriv_at c c' x) (hd : has_strict_deriv_at d d' x) (hx : d x β‰  0) :
has_strict_deriv_at (Ξ» (y : π•œ), c y / d y) ((c' * d x - (c x) * d') / d x ^ 2) x
theorem has_deriv_at.div {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} {c d : π•œ β†’ π•œ} {c' d' : π•œ} (hc : has_deriv_at c c' x) (hd : has_deriv_at d d' x) (hx : 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 : π•œ β†’ π•œ} (hc : differentiable_within_at π•œ c s x) (hd : differentiable_within_at π•œ d s x) (hx : 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 : π•œ β†’ π•œ} (hc : differentiable_at π•œ c x) (hd : differentiable_at π•œ d x) (hx : d x β‰  0) :
differentiable_at π•œ (Ξ» (x : π•œ), c x / d x) x
theorem differentiable_on.div {π•œ : Type u} [nondiscrete_normed_field π•œ] {s : set π•œ} {c d : π•œ β†’ π•œ} (hc : differentiable_on π•œ c s) (hd : differentiable_on π•œ d s) (hx : βˆ€ (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 : π•œ β†’ π•œ} (hc : differentiable π•œ c) (hd : differentiable π•œ d) (hx : βˆ€ (x : π•œ), d x β‰  0) :
differentiable π•œ (Ξ» (x : π•œ), c x / d x)
theorem deriv_within_div {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} {s : set π•œ} {c d : π•œ β†’ π•œ} (hc : differentiable_within_at π•œ c s x) (hd : differentiable_within_at π•œ d s x) (hx : d x β‰  0) (hxs : 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
@[simp]
theorem deriv_div {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} {c d : π•œ β†’ π•œ} (hc : differentiable_at π•œ c x) (hd : differentiable_at π•œ d x) (hx : d x β‰  0) :
deriv (Ξ» (x : π•œ), c x / d x) x = ((deriv c x) * d x - (c x) * deriv d 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 : π•œ} (hxs : 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 : π•œ β†’ π•œ} (d : π•œ) :
deriv (Ξ» (x : π•œ), c x / d) x = deriv c x / d

Derivative of the pointwise composition/application of continuous linear maps #

theorem has_strict_deriv_at.clm_comp {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {E : Type w} [normed_group E] [normed_space π•œ E] {x : π•œ} {G : Type u_1} [normed_group G] [normed_space π•œ G] {c : π•œ β†’ (F β†’L[π•œ] G)} {c' : F β†’L[π•œ] G} {d : π•œ β†’ (E β†’L[π•œ] F)} {d' : E β†’L[π•œ] F} (hc : has_strict_deriv_at c c' x) (hd : has_strict_deriv_at d d' x) :
has_strict_deriv_at (Ξ» (y : π•œ), (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') x
theorem has_deriv_within_at.clm_comp {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {E : Type w} [normed_group E] [normed_space π•œ E] {x : π•œ} {s : set π•œ} {G : Type u_1} [normed_group G] [normed_space π•œ G] {c : π•œ β†’ (F β†’L[π•œ] G)} {c' : F β†’L[π•œ] G} {d : π•œ β†’ (E β†’L[π•œ] F)} {d' : E β†’L[π•œ] F} (hc : has_deriv_within_at c c' s x) (hd : has_deriv_within_at d d' s x) :
has_deriv_within_at (Ξ» (y : π•œ), (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') s x
theorem has_deriv_at.clm_comp {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {E : Type w} [normed_group E] [normed_space π•œ E] {x : π•œ} {G : Type u_1} [normed_group G] [normed_space π•œ G] {c : π•œ β†’ (F β†’L[π•œ] G)} {c' : F β†’L[π•œ] G} {d : π•œ β†’ (E β†’L[π•œ] F)} {d' : E β†’L[π•œ] F} (hc : has_deriv_at c c' x) (hd : has_deriv_at d d' x) :
has_deriv_at (Ξ» (y : π•œ), (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') x
theorem deriv_within_clm_comp {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {E : Type w} [normed_group E] [normed_space π•œ E] {x : π•œ} {s : set π•œ} {G : Type u_1} [normed_group G] [normed_space π•œ G] {c : π•œ β†’ (F β†’L[π•œ] G)} {d : π•œ β†’ (E β†’L[π•œ] F)} (hc : differentiable_within_at π•œ c s x) (hd : differentiable_within_at π•œ d s x) (hxs : unique_diff_within_at π•œ s x) :
deriv_within (Ξ» (y : π•œ), (c y).comp (d y)) s x = (deriv_within c s x).comp (d x) + (c x).comp (deriv_within d s x)
theorem deriv_clm_comp {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {E : Type w} [normed_group E] [normed_space π•œ E] {x : π•œ} {G : Type u_1} [normed_group G] [normed_space π•œ G] {c : π•œ β†’ (F β†’L[π•œ] G)} {d : π•œ β†’ (E β†’L[π•œ] F)} (hc : differentiable_at π•œ c x) (hd : differentiable_at π•œ d x) :
deriv (Ξ» (y : π•œ), (c y).comp (d y)) x = (deriv c x).comp (d x) + (c x).comp (deriv d x)
theorem has_strict_deriv_at.clm_apply {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {x : π•œ} {G : Type u_1} [normed_group G] [normed_space π•œ G] {c : π•œ β†’ (F β†’L[π•œ] G)} {c' : F β†’L[π•œ] G} {u : π•œ β†’ F} {u' : F} (hc : has_strict_deriv_at c c' x) (hu : has_strict_deriv_at u u' x) :
has_strict_deriv_at (Ξ» (y : π•œ), ⇑(c y) (u y)) (⇑c' (u x) + ⇑(c x) u') x
theorem has_deriv_within_at.clm_apply {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {x : π•œ} {s : set π•œ} {G : Type u_1} [normed_group G] [normed_space π•œ G] {c : π•œ β†’ (F β†’L[π•œ] G)} {c' : F β†’L[π•œ] G} {u : π•œ β†’ F} {u' : F} (hc : has_deriv_within_at c c' s x) (hu : has_deriv_within_at u u' s x) :
has_deriv_within_at (Ξ» (y : π•œ), ⇑(c y) (u y)) (⇑c' (u x) + ⇑(c x) u') s x
theorem has_deriv_at.clm_apply {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {x : π•œ} {G : Type u_1} [normed_group G] [normed_space π•œ G] {c : π•œ β†’ (F β†’L[π•œ] G)} {c' : F β†’L[π•œ] G} {u : π•œ β†’ F} {u' : F} (hc : has_deriv_at c c' x) (hu : has_deriv_at u u' x) :
has_deriv_at (Ξ» (y : π•œ), ⇑(c y) (u y)) (⇑c' (u x) + ⇑(c x) u') x
theorem deriv_within_clm_apply {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {x : π•œ} {s : set π•œ} {G : Type u_1} [normed_group G] [normed_space π•œ G] {c : π•œ β†’ (F β†’L[π•œ] G)} {u : π•œ β†’ F} (hxs : unique_diff_within_at π•œ s x) (hc : differentiable_within_at π•œ c s x) (hu : differentiable_within_at π•œ u s x) :
deriv_within (Ξ» (y : π•œ), ⇑(c y) (u y)) s x = ⇑(deriv_within c s x) (u x) + ⇑(c x) (deriv_within u s x)
theorem deriv_clm_apply {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {x : π•œ} {G : Type u_1} [normed_group G] [normed_space π•œ G] {c : π•œ β†’ (F β†’L[π•œ] G)} {u : π•œ β†’ F} (hc : differentiable_at π•œ c x) (hu : differentiable_at π•œ u x) :
deriv (Ξ» (y : π•œ), ⇑(c y) (u y)) x = ⇑(deriv c x) (u x) + ⇑(c x) (deriv u x)
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) :
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) :
theorem has_strict_deriv_at.of_local_left_inverse {π•œ : Type u} [nondiscrete_normed_field π•œ] {f g : π•œ β†’ π•œ} {f' a : π•œ} (hg : continuous_at g a) (hf : has_strict_deriv_at f f' (g a)) (hf' : f' β‰  0) (hfg : βˆ€αΆ  (y : π•œ) in 𝓝 a, f (g y) = y) :

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 local_homeomorph.has_strict_deriv_at_symm {π•œ : Type u} [nondiscrete_normed_field π•œ] (f : local_homeomorph π•œ π•œ) {a f' : π•œ} (ha : a ∈ f.to_local_equiv.target) (hf' : f' β‰  0) (htff' : has_strict_deriv_at ⇑f f' (⇑(f.symm) a)) :

If f is a local homeomorphism defined on a neighbourhood of f.symm a, and f has a nonzero derivative f' at f.symm a in the strict sense, then f.symm 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 : π•œ} (hg : continuous_at g a) (hf : has_deriv_at f f' (g a)) (hf' : f' β‰  0) (hfg : βˆ€αΆ  (y : π•œ) in 𝓝 a, f (g y) = y) :

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.

theorem local_homeomorph.has_deriv_at_symm {π•œ : Type u} [nondiscrete_normed_field π•œ] (f : local_homeomorph π•œ π•œ) {a f' : π•œ} (ha : a ∈ f.to_local_equiv.target) (hf' : f' β‰  0) (htff' : has_deriv_at ⇑f f' (⇑(f.symm) a)) :

If f is a local homeomorphism defined on a neighbourhood of f.symm a, and f has an nonzero derivative f' at f.symm a, then f.symm 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.

theorem has_deriv_at.eventually_ne {π•œ : Type u} [nondiscrete_normed_field π•œ] {F : Type v} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} (h : has_deriv_at f f' x) (hf' : f' β‰  0) :
βˆ€αΆ  (z : π•œ) in 𝓝[{x}ᢜ] x, f z β‰  f x
theorem not_differentiable_within_at_of_local_left_inverse_has_deriv_within_at_zero {π•œ : Type u} [nondiscrete_normed_field π•œ] {f g : π•œ β†’ π•œ} {a : π•œ} {s t : set π•œ} (ha : a ∈ s) (hsu : unique_diff_within_at π•œ s a) (hf : has_deriv_within_at f 0 t (g a)) (hst : set.maps_to g s t) (hfg : f ∘ g =αΆ [𝓝[s] a] id) :
theorem not_differentiable_at_of_local_left_inverse_has_deriv_at_zero {π•œ : Type u} [nondiscrete_normed_field π•œ] {f g : π•œ β†’ π•œ} {a : π•œ} (hf : has_deriv_at f 0 (g a)) (hfg : f ∘ g =αΆ [𝓝 a] id) :

Derivative of a polynomial #

theorem polynomial.has_strict_deriv_at {π•œ : Type u} [nondiscrete_normed_field π•œ] (p : polynomial π•œ) (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 : π•œ) :

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 π•œ) :
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 π•œ) :
theorem polynomial.deriv_within {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} {s : set π•œ} (p : polynomial π•œ) (hxs : unique_diff_within_at π•œ s x) :
theorem polynomial.has_fderiv_at {π•œ : Type u} [nondiscrete_normed_field π•œ] (p : polynomial π•œ) (x : π•œ) :
theorem polynomial.has_fderiv_within_at {π•œ : Type u} [nondiscrete_normed_field π•œ] {s : set π•œ} (p : polynomial π•œ) (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 (⇑polynomial.derivative p))
theorem polynomial.fderiv_within {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} {s : set π•œ} (p : polynomial π•œ) (hxs : unique_diff_within_at π•œ s x) :
fderiv_within π•œ (Ξ» (x : π•œ), polynomial.eval x p) s x = 1.smul_right (polynomial.eval x (⇑polynomial.derivative p))

Derivative of x ↦ x^n for n : β„• #

theorem has_strict_deriv_at_pow {π•œ : Type u} [nondiscrete_normed_field π•œ] (n : β„•) (x : π•œ) :
has_strict_deriv_at (Ξ» (x : π•œ), x ^ n) ((↑n) * x ^ (n - 1)) x
theorem has_deriv_at_pow {π•œ : Type u} [nondiscrete_normed_field π•œ] (n : β„•) (x : π•œ) :
has_deriv_at (Ξ» (x : π•œ), x ^ n) ((↑n) * x ^ (n - 1)) x
theorem has_deriv_within_at_pow {π•œ : Type u} [nondiscrete_normed_field π•œ] (n : β„•) (x : π•œ) (s : set π•œ) :
has_deriv_within_at (Ξ» (x : π•œ), x ^ n) ((↑n) * x ^ (n - 1)) s x
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_pow {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} {n : β„•} :
deriv (Ξ» (x : π•œ), x ^ n) x = (↑n) * x ^ (n - 1)
@[simp]
theorem deriv_pow' {π•œ : Type u} [nondiscrete_normed_field π•œ] {n : β„•} :
deriv (Ξ» (x : π•œ), x ^ n) = Ξ» (x : π•œ), (↑n) * x ^ (n - 1)
theorem deriv_within_pow {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} {s : set π•œ} {n : β„•} (hxs : 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 : β„•} (hc : 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 : β„•} (hc : 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 : β„•} (hc : 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 : β„•} (hc : differentiable_at π•œ c x) :
differentiable_at π•œ (Ξ» (x : π•œ), c x ^ n) x
theorem differentiable_on.pow {π•œ : Type u} [nondiscrete_normed_field π•œ] {s : set π•œ} {c : π•œ β†’ π•œ} {n : β„•} (hc : differentiable_on π•œ c s) :
differentiable_on π•œ (Ξ» (x : π•œ), c x ^ n) s
@[simp]
theorem differentiable.pow {π•œ : Type u} [nondiscrete_normed_field π•œ] {c : π•œ β†’ π•œ} {n : β„•} (hc : differentiable π•œ c) :
differentiable π•œ (Ξ» (x : π•œ), c x ^ n)
theorem deriv_within_pow' {π•œ : Type u} [nondiscrete_normed_field π•œ] {x : π•œ} {s : set π•œ} {c : π•œ β†’ π•œ} {n : β„•} (hc : differentiable_within_at π•œ c s x) (hxs : 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 : β„•} (hc : differentiable_at π•œ c x) :
deriv (Ξ» (x : π•œ), c x ^ n) x = ((↑n) * c x ^ (n - 1)) * deriv c x

Derivative of x ↦ x^m for m : β„€ #

theorem has_strict_deriv_at_fpow {π•œ : Type u} [nondiscrete_normed_field π•œ] (m : β„€) (x : π•œ) (h : x β‰  0 ∨ 0 ≀ m) :
has_strict_deriv_at (Ξ» (x : π•œ), x ^ m) ((