# Documentation

Mathlib.Analysis.Calculus.IteratedDeriv

# One-dimensional iterated derivatives #

We define the n-th derivative of a function f : π β F as a function iteratedDeriv n f : π β F, as well as a version on domains iteratedDerivWithin n f s : π β F, and prove their basic properties.

## Main definitions and results #

Let π be a nontrivially normed field, and F a normed vector space over π. Let f : π β F.

• iteratedDeriv n f is the n-th derivative of f, seen as a function from π to F. It is defined as the n-th FrΓ©chet derivative (which is a multilinear map) applied to the vector (1, ..., 1), to take advantage of all the existing framework, but we show that it coincides with the naive iterative definition.
• iteratedDeriv_eq_iterate states that the n-th derivative of f is obtained by starting from f and differentiating it n times.
• iteratedDerivWithin n f s is the n-th derivative of f within the domain s. It only behaves well when s has the unique derivative property.
• iteratedDerivWithin_eq_iterate states that the n-th derivative of f in the domain s is obtained by starting from f and differentiating it n times within s. This only holds when s has the unique derivative property.

## Implementation details #

The results are deduced from the corresponding results for the more general (multilinear) iterated FrΓ©chet derivative. For this, we write iteratedDeriv n f as the composition of iteratedFDeriv π 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 iteratedDerivWithin_succ, by translating the corresponding result iteratedFDerivWithin_succ_apply_left for the iterated FrΓ©chet derivative.

def iteratedDeriv {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] (n : β) (f : π β F) (x : π) :
F

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

Instances For
def iteratedDerivWithin {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] (n : β) (f : π β F) (s : Set π) (x : π) :
F

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

Instances For
theorem iteratedDerivWithin_univ {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {n : β} {f : π β F} :
iteratedDerivWithin n f Set.univ =

### Properties of the iterated derivative within a set #

theorem iteratedDerivWithin_eq_iteratedFDerivWithin {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {n : β} {f : π β F} {s : Set π} {x : π} :
= β(iteratedFDerivWithin π n f s x) fun x => 1
theorem iteratedDerivWithin_eq_equiv_comp {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {n : β} {f : π β F} {s : Set π} :
= β() β iteratedFDerivWithin π n f s

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

theorem iteratedFDerivWithin_eq_equiv_comp {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {n : β} {f : π β F} {s : Set π} :
iteratedFDerivWithin π n f s = β() β

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

theorem iteratedFDerivWithin_apply_eq_iteratedDerivWithin_mul_prod {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {n : β} {f : π β F} {s : Set π} {x : π} {m : Fin n β π} :
β(iteratedFDerivWithin π n f s x) m = (Finset.prod Finset.univ fun i => m i) β’

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.

theorem norm_iteratedFDerivWithin_eq_norm_iteratedDerivWithin {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {n : β} {f : π β F} {s : Set π} {x : π} :
@[simp]
theorem iteratedDerivWithin_zero {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {f : π β F} {s : Set π} :
= f
@[simp]
theorem iteratedDerivWithin_one {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {f : π β F} {s : Set π} {x : π} (h : UniqueDiffWithinAt π s x) :
= derivWithin f s x
theorem contDiffOn_of_continuousOn_differentiableOn_deriv {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {f : π β F} {s : Set π} {n : ββ} (Hcont : β (m : β), βm β€ n β ContinuousOn (fun x => ) s) (Hdiff : β (m : β), βm < n β DifferentiableOn π (fun x => ) s) :
ContDiffOn π 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 contDiffOn_iff_continuousOn_differentiableOn_deriv.

theorem contDiffOn_of_differentiableOn_deriv {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {f : π β F} {s : Set π} {n : ββ} (h : β (m : β), βm β€ n β DifferentiableOn π () s) :
ContDiffOn π 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 ContDiffOn.continuousOn_iteratedDerivWithin {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {f : π β F} {s : Set π} {n : ββ} {m : β} (h : ContDiffOn π n f s) (hmn : βm β€ n) (hs : UniqueDiffOn π s) :

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

theorem ContDiffWithinAt.differentiableWithinAt_iteratedDerivWithin {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {f : π β F} {s : Set π} {x : π} {n : ββ} {m : β} (h : ContDiffWithinAt π n f s x) (hmn : βm < n) (hs : UniqueDiffOn π (insert x s)) :
DifferentiableWithinAt π () s x
theorem ContDiffOn.differentiableOn_iteratedDerivWithin {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {f : π β F} {s : Set π} {n : ββ} {m : β} (h : ContDiffOn π n f s) (hmn : βm < n) (hs : UniqueDiffOn π s) :
DifferentiableOn π () s

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

theorem contDiffOn_iff_continuousOn_differentiableOn_deriv {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {f : π β F} {s : Set π} {n : ββ} (hs : UniqueDiffOn π s) :
ContDiffOn π n f s β (β (m : β), βm β€ n β ContinuousOn () s) β§ β (m : β), βm < n β DifferentiableOn π () 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 iteratedDerivWithin_succ {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {n : β} {f : π β F} {s : Set π} {x : π} (hxs : UniqueDiffWithinAt π s x) :
iteratedDerivWithin (n + 1) f s x = derivWithin () s x

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

theorem iteratedDerivWithin_eq_iterate {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {n : β} {f : π β F} {s : Set π} {x : π} (hs : UniqueDiffOn π s) (hx : x β s) :
= (π β F)^[fun g => ] 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 iteratedDerivWithin_succ' {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {n : β} {f : π β F} {s : Set π} {x : π} (hxs : UniqueDiffOn π s) (hx : x β s) :

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 iteratedDeriv_eq_iteratedFDeriv {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {n : β} {f : π β F} {x : π} :
= β(iteratedFDeriv π n f x) fun x => 1
theorem iteratedDeriv_eq_equiv_comp {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {n : β} {f : π β F} :
= β() β iteratedFDeriv π n f

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

theorem iteratedFDeriv_eq_equiv_comp {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {n : β} {f : π β F} :
iteratedFDeriv π n f = β() β

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

theorem iteratedFDeriv_apply_eq_iteratedDeriv_mul_prod {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {n : β} {f : π β F} {x : π} {m : Fin n β π} :
β(iteratedFDeriv π n f x) m = (Finset.prod Finset.univ fun i => m i) β’

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.

theorem norm_iteratedFDeriv_eq_norm_iteratedDeriv {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {n : β} {f : π β F} {x : π} :
@[simp]
theorem iteratedDeriv_zero {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {f : π β F} :
= f
@[simp]
theorem iteratedDeriv_one {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {f : π β F} :
=
theorem contDiff_iff_iteratedDeriv {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {f : π β F} {n : ββ} :
ContDiff π n f β (β (m : β), βm β€ n β Continuous ()) β§ β (m : β), βm < n β Differentiable π ()

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 contDiff_of_differentiable_iteratedDeriv {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {f : π β F} {n : ββ} (h : β (m : β), βm β€ n β Differentiable π ()) :
ContDiff π 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 ContDiff.continuous_iteratedDeriv {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {f : π β F} {n : ββ} (m : β) (h : ContDiff π n f) (hmn : βm β€ n) :
theorem ContDiff.differentiable_iteratedDeriv {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {f : π β F} {n : ββ} (m : β) (h : ContDiff π n f) (hmn : βm < n) :
Differentiable π ()
theorem iteratedDeriv_succ {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {n : β} {f : π β F} :
iteratedDeriv (n + 1) f = deriv ()

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

theorem iteratedDeriv_eq_iterate {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {n : β} {f : π β F} :

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

theorem iteratedDeriv_succ' {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {n : β} {f : π β F} :

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