mathlib documentation

analysis.calculus.iterated_deriv

One-dimensional iterated derivatives

We define the n-th derivative of a function f : π•œ β†’ F as a function iterated_deriv n f : π•œ β†’ F, as well as a version on domains iterated_deriv_within n f s : π•œ β†’ F, and prove their basic properties.

Main definitions and results

Let π•œ be a nondiscrete normed field, and F a normed vector space over π•œ. Let f : π•œ β†’ F.

Implementation details

The results are deduced from the corresponding results for the more general (multilinear) iterated FrΓ©chet derivative. For this, we write iterated_deriv n f as the composition of iterated_fderiv π•œ n f and a continuous linear equiv. As continuous linear equivs respect differentiability and commute with differentiation, this makes it possible to prove readily that the derivative of the n-th derivative is the n+1-th derivative in iterated_deriv_within_succ, by translating the corresponding result iterated_fderiv_within_succ_apply_left for the iterated FrΓ©chet derivative.

def iterated_deriv {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] :
β„• β†’ (π•œ β†’ F) β†’ π•œ β†’ F

The n-th iterated derivative of a function from π•œ to F, as a function from π•œ to F.

Equations
def iterated_deriv_within {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] :
β„• β†’ (π•œ β†’ F) β†’ set π•œ β†’ π•œ β†’ F

The n-th iterated derivative of a function from π•œ to F within a set s, as a function from π•œ to F.

Equations
theorem iterated_deriv_within_univ {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] {n : β„•} {f : π•œ β†’ F} :

Properties of the iterated derivative within a set

theorem iterated_deriv_within_eq_iterated_fderiv_within {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] {n : β„•} {f : π•œ β†’ F} {s : set π•œ} {x : π•œ} :
iterated_deriv_within n f s x = ⇑(iterated_fderiv_within π•œ n f s x) (Ξ» (i : fin n), 1)

theorem iterated_deriv_within_eq_equiv_comp {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] {n : β„•} {f : π•œ β†’ F} {s : set π•œ} :

Write the iterated derivative as the composition of a continuous linear equiv and the iterated FrΓ©chet derivative

theorem iterated_fderiv_within_eq_equiv_comp {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] {n : β„•} {f : π•œ β†’ F} {s : set π•œ} :

Write the iterated FrΓ©chet derivative as the composition of a continuous linear equiv and the iterated derivative.

theorem iterated_fderiv_within_apply_eq_iterated_deriv_within_mul_prod {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] {n : β„•} {f : π•œ β†’ F} {s : set π•œ} {x : π•œ} {m : fin n β†’ π•œ} :
⇑(iterated_fderiv_within π•œ n f s x) m = (∏ (i : fin n), m i) β€’ iterated_deriv_within n f s x

The n-th FrΓ©chet derivative applied to a vector (m 0, ..., m (n-1)) is the derivative multiplied by the product of the m is.

@[simp]
theorem iterated_deriv_within_zero {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {s : set π•œ} :

@[simp]
theorem iterated_deriv_within_one {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {s : set π•œ} (hs : unique_diff_on π•œ s) {x : π•œ} :
x ∈ s β†’ iterated_deriv_within 1 f s x = deriv_within f s x

theorem times_cont_diff_on_of_continuous_on_differentiable_on_deriv {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {s : set π•œ} {n : with_top β„•} :
(βˆ€ (m : β„•), ↑m ≀ n β†’ continuous_on (Ξ» (x : π•œ), iterated_deriv_within m f s x) s) β†’ (βˆ€ (m : β„•), ↑m < n β†’ differentiable_on π•œ (Ξ» (x : π•œ), iterated_deriv_within m f s x) s) β†’ times_cont_diff_on π•œ n f s

If the first n derivatives within a set of a function are continuous, and its first n-1 derivatives are differentiable, then the function is C^n. This is not an equivalence in general, but this is an equivalence when the set has unique derivatives, see times_cont_diff_on_iff_continuous_on_differentiable_on_deriv.

theorem times_cont_diff_on_of_differentiable_on_deriv {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {s : set π•œ} {n : with_top β„•} :
(βˆ€ (m : β„•), ↑m ≀ n β†’ differentiable_on π•œ (iterated_deriv_within m f s) s) β†’ times_cont_diff_on π•œ n f s

To check that a function is n times continuously differentiable, it suffices to check that its first n derivatives are differentiable. This is slightly too strong as the condition we require on the n-th derivative is differentiability instead of continuity, but it has the advantage of avoiding the discussion of continuity in the proof (and for n = ∞ this is optimal).

theorem times_cont_diff_on.continuous_on_iterated_deriv_within {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {s : set π•œ} {n : with_top β„•} {m : β„•} :
times_cont_diff_on π•œ n f s β†’ ↑m ≀ n β†’ unique_diff_on π•œ s β†’ continuous_on (iterated_deriv_within m f s) s

On a set with unique derivatives, a C^n function has derivatives up to n which are continuous.

theorem times_cont_diff_on.differentiable_on_iterated_deriv_within {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {s : set π•œ} {n : with_top β„•} {m : β„•} :
times_cont_diff_on π•œ n f s β†’ ↑m < n β†’ unique_diff_on π•œ s β†’ differentiable_on π•œ (iterated_deriv_within m f s) s

On a set with unique derivatives, a C^n function has derivatives less than n which are differentiable.

theorem times_cont_diff_on_iff_continuous_on_differentiable_on_deriv {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {s : set π•œ} {n : with_top β„•} :
unique_diff_on π•œ s β†’ (times_cont_diff_on π•œ n f s ↔ (βˆ€ (m : β„•), ↑m ≀ n β†’ continuous_on (iterated_deriv_within m f s) s) ∧ βˆ€ (m : β„•), ↑m < n β†’ differentiable_on π•œ (iterated_deriv_within m f s) s)

The property of being C^n, initially defined in terms of the FrΓ©chet derivative, can be reformulated in terms of the one-dimensional derivative on sets with unique derivatives.

theorem iterated_deriv_within_succ {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] {n : β„•} {f : π•œ β†’ F} {s : set π•œ} {x : π•œ} :

The n+1-th iterated derivative within a set with unique derivatives can be obtained by differentiating the n-th iterated derivative.

theorem iterated_deriv_within_eq_iterate {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] {n : β„•} {f : π•œ β†’ F} {s : set π•œ} {x : π•œ} :
unique_diff_on π•œ s β†’ x ∈ s β†’ iterated_deriv_within n f s x = (Ξ» (g : π•œ β†’ F), deriv_within g s)^[n] f x

The n-th iterated derivative within a set with unique derivatives can be obtained by iterating n times the differentiation operation.

theorem iterated_deriv_within_succ' {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] {n : β„•} {f : π•œ β†’ F} {s : set π•œ} {x : π•œ} :
unique_diff_on π•œ s β†’ x ∈ s β†’ iterated_deriv_within (n + 1) f s x = iterated_deriv_within n (deriv_within f s) s x

The n+1-th iterated derivative within a set with unique derivatives can be obtained by taking the n-th derivative of the derivative.

Properties of the iterated derivative on the whole space

theorem iterated_deriv_eq_iterated_fderiv {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] {n : β„•} {f : π•œ β†’ F} {x : π•œ} :
iterated_deriv n f x = ⇑(iterated_fderiv π•œ n f x) (Ξ» (i : fin n), 1)

theorem iterated_deriv_eq_equiv_comp {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] {n : β„•} {f : π•œ β†’ F} :

Write the iterated derivative as the composition of a continuous linear equiv and the iterated FrΓ©chet derivative

theorem iterated_fderiv_eq_equiv_comp {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] {n : β„•} {f : π•œ β†’ F} :

Write the iterated FrΓ©chet derivative as the composition of a continuous linear equiv and the iterated derivative.

theorem iterated_fderiv_apply_eq_iterated_deriv_mul_prod {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] {n : β„•} {f : π•œ β†’ F} {x : π•œ} {m : fin n β†’ π•œ} :
⇑(iterated_fderiv π•œ n f x) m = (∏ (i : fin n), m i) β€’ iterated_deriv n f x

The n-th FrΓ©chet derivative applied to a vector (m 0, ..., m (n-1)) is the derivative multiplied by the product of the m is.

@[simp]
theorem iterated_deriv_zero {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} :

@[simp]
theorem iterated_deriv_one {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} :

theorem times_cont_diff_iff_iterated_deriv {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {n : with_top β„•} :
times_cont_diff π•œ n f ↔ (βˆ€ (m : β„•), ↑m ≀ n β†’ continuous (iterated_deriv m f)) ∧ βˆ€ (m : β„•), ↑m < n β†’ differentiable π•œ (iterated_deriv m f)

The property of being C^n, initially defined in terms of the FrΓ©chet derivative, can be reformulated in terms of the one-dimensional derivative.

theorem times_cont_diff_of_differentiable_iterated_deriv {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {n : with_top β„•} :
(βˆ€ (m : β„•), ↑m ≀ n β†’ differentiable π•œ (iterated_deriv m f)) β†’ times_cont_diff π•œ n f

To check that a function is n times continuously differentiable, it suffices to check that its first n derivatives are differentiable. This is slightly too strong as the condition we require on the n-th derivative is differentiability instead of continuity, but it has the advantage of avoiding the discussion of continuity in the proof (and for n = ∞ this is optimal).

theorem times_cont_diff.continuous_iterated_deriv {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {n : with_top β„•} (m : β„•) :
times_cont_diff π•œ n f β†’ ↑m ≀ n β†’ continuous (iterated_deriv m f)

theorem times_cont_diff.differentiable_iterated_deriv {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] {f : π•œ β†’ F} {n : with_top β„•} (m : β„•) :
times_cont_diff π•œ n f β†’ ↑m < n β†’ differentiable π•œ (iterated_deriv m f)

theorem iterated_deriv_succ {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] {n : β„•} {f : π•œ β†’ F} :

The n+1-th iterated derivative can be obtained by differentiating the n-th iterated derivative.

theorem iterated_deriv_eq_iterate {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] {n : β„•} {f : π•œ β†’ F} :

The n-th iterated derivative can be obtained by iterating n times the differentiation operation.

theorem iterated_deriv_succ' {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {F : Type u_2} [normed_group F] [normed_space π•œ F] {n : β„•} {f : π•œ β†’ F} :

The n+1-th iterated derivative can be obtained by taking the n-th derivative of the derivative.