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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) (f : 𝕜 → F) (x : 𝕜) : F

The n-th iterated derivative of a function from 𝕜 to F, as a function from 𝕜 to F.

Equations

• iteratedDeriv n f x = (iteratedFDeriv 𝕜 n f x) fun (x : Fin n) => 1

def iteratedDerivWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [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.

Equations

• iteratedDerivWithin n f s x = (iteratedFDerivWithin 𝕜 n f s x) fun (x : Fin n) => 1

theorem iteratedDerivWithin_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} : iteratedDerivWithin n f Set.univ = iteratedDeriv n f

theorem iteratedDerivWithin_eq_iteratedDeriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {s : Set 𝕜} {x : 𝕜} (hs : UniqueDiffOn 𝕜 s) (h : ContDiffAt 𝕜 (↑n) f x) (hx : x ∈ s) : iteratedDerivWithin n f s x = iteratedDeriv n f x

Properties of the iterated derivative within a set

theorem iteratedDerivWithin_eq_iteratedFDerivWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {s : Set 𝕜} {x : 𝕜} : iteratedDerivWithin n f s x = (iteratedFDerivWithin 𝕜 n f s x) fun (x : Fin n) => 1

theorem iteratedDerivWithin_eq_equiv_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {s : Set 𝕜} : iteratedDerivWithin n f s = ⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F).symm ∘ 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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {s : Set 𝕜} : iteratedFDerivWithin 𝕜 n f s = ⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) ∘ iteratedDerivWithin 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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {s : Set 𝕜} {x : 𝕜} {m : Fin n → 𝕜} : (iteratedFDerivWithin 𝕜 n f s x) m = (∏ i : Fin n, m i) • iteratedDerivWithin 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.

theorem norm_iteratedFDerivWithin_eq_norm_iteratedDerivWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {s : Set 𝕜} {x : 𝕜} : ‖iteratedFDerivWithin 𝕜 n f s x‖ = ‖iteratedDerivWithin n f s x‖

@[simp]

theorem iteratedDerivWithin_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} : iteratedDerivWithin 0 f s = f

@[simp]

theorem iteratedDerivWithin_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} {x : 𝕜} : iteratedDerivWithin 1 f s x = derivWithin f s x

theorem contDiffOn_of_continuousOn_differentiableOn_deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} {n : ℕ∞} (Hcont : ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun (x : 𝕜) => iteratedDerivWithin m f s x) s) (Hdiff : ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun (x : 𝕜) => iteratedDerivWithin m f s 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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} {n : ℕ∞} (h : ∀ (m : ℕ), ↑m ≤ n → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) 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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} {n : WithTop ℕ∞} {m : ℕ} (h : ContDiffOn 𝕜 n f s) (hmn : ↑m ≤ n) (hs : UniqueDiffOn 𝕜 s) : ContinuousOn (iteratedDerivWithin m f s) 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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} {x : 𝕜} {n : WithTop ℕ∞} {m : ℕ} (h : ContDiffWithinAt 𝕜 n f s x) (hmn : ↑m < n) (hs : UniqueDiffOn 𝕜 (insert x s)) : DifferentiableWithinAt 𝕜 (iteratedDerivWithin m f s) s x

theorem ContDiffOn.differentiableOn_iteratedDerivWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} {n : WithTop ℕ∞} {m : ℕ} (h : ContDiffOn 𝕜 n f s) (hmn : ↑m < n) (hs : UniqueDiffOn 𝕜 s) : DifferentiableOn 𝕜 (iteratedDerivWithin m f s) 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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} {n : ℕ∞} (hs : UniqueDiffOn 𝕜 s) : ContDiffOn 𝕜 (↑n) f s ↔ (∀ (m : ℕ), ↑m ≤ n → ContinuousOn (iteratedDerivWithin m f s) s) ∧ ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (iteratedDerivWithin 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 contDiffOn_nat_iff_continuousOn_differentiableOn_deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} {n : ℕ} (hs : UniqueDiffOn 𝕜 s) : ContDiffOn 𝕜 (↑n) f s ↔ (∀ m ≤ n, ContinuousOn (iteratedDerivWithin m f s) s) ∧ ∀ m < n, DifferentiableOn 𝕜 (iteratedDerivWithin 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 iteratedDerivWithin_succ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {s : Set 𝕜} {x : 𝕜} : iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) 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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {s : Set 𝕜} {x : 𝕜} : iteratedDerivWithin n f s x = (fun (g : 𝕜 → F) => derivWithin 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 iteratedDerivWithin_succ' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {s : Set 𝕜} {x : 𝕜} : iteratedDerivWithin (n + 1) f s x = iteratedDerivWithin n (derivWithin 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 iteratedDeriv_eq_iteratedFDeriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {x : 𝕜} : iteratedDeriv n f x = (iteratedFDeriv 𝕜 n f x) fun (x : Fin n) => 1

theorem iteratedDeriv_eq_equiv_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} : iteratedDeriv n f = ⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F).symm ∘ 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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} : iteratedFDeriv 𝕜 n f = ⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) ∘ iteratedDeriv 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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {x : 𝕜} {m : Fin n → 𝕜} : (iteratedFDeriv 𝕜 n f x) m = (∏ i : Fin n, m i) • iteratedDeriv 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.

theorem norm_iteratedFDeriv_eq_norm_iteratedDeriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {x : 𝕜} : ‖iteratedFDeriv 𝕜 n f x‖ = ‖iteratedDeriv n f x‖

@[simp]

theorem iteratedDeriv_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} : iteratedDeriv 0 f = f

@[simp]

theorem iteratedDeriv_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} : iteratedDeriv 1 f = deriv f

theorem contDiff_iff_iteratedDeriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {n : ℕ∞} : ContDiff 𝕜 (↑n) f ↔ (∀ (m : ℕ), ↑m ≤ n → Continuous (iteratedDeriv m f)) ∧ ∀ (m : ℕ), ↑m < n → Differentiable 𝕜 (iteratedDeriv 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 contDiff_nat_iff_iteratedDeriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {n : ℕ} : ContDiff 𝕜 (↑n) f ↔ (∀ m ≤ n, Continuous (iteratedDeriv m f)) ∧ ∀ m < n, Differentiable 𝕜 (iteratedDeriv 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 contDiff_of_differentiable_iteratedDeriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {n : ℕ∞} (h : ∀ (m : ℕ), ↑m ≤ n → Differentiable 𝕜 (iteratedDeriv m f)) : 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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {n : WithTop ℕ∞} (m : ℕ) (h : ContDiff 𝕜 n f) (hmn : ↑m ≤ n) : Continuous (iteratedDeriv m f)

theorem ContDiff.continuous_iteratedDeriv' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} (m : ℕ) (h : ContDiff 𝕜 (↑m) f) : Continuous (iteratedDeriv m f)

theorem ContDiff.differentiable_iteratedDeriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {n : WithTop ℕ∞} (m : ℕ) (h : ContDiff 𝕜 n f) (hmn : ↑m < n) : Differentiable 𝕜 (iteratedDeriv m f)

theorem ContDiff.differentiable_iteratedDeriv' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} (m : ℕ) (h : ContDiff 𝕜 (↑m + 1) f) : Differentiable 𝕜 (iteratedDeriv m f)

theorem iteratedDeriv_succ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} : iteratedDeriv (n + 1) f = deriv (iteratedDeriv n f)

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

theorem iteratedDeriv_eq_iterate {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} : iteratedDeriv n f = deriv^[n] f

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

theorem iteratedDerivWithin_of_isOpen {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {s : Set 𝕜} (hs : IsOpen s) : Set.EqOn (iteratedDerivWithin n f s) (iteratedDeriv n f) s

theorem iteratedDerivWithin_congr_right_of_isOpen {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : 𝕜 → F) (n : ℕ) {s t : Set 𝕜} (hs : IsOpen s) (ht : IsOpen t) : Set.EqOn (iteratedDerivWithin n f s) (iteratedDerivWithin n f t) (s ∩ t)

theorem iteratedDerivWithin_of_isOpen_eq_iterate {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {s : Set 𝕜} (hs : IsOpen s) : Set.EqOn (iteratedDerivWithin n f s) (deriv^[n] f) s

theorem iteratedDeriv_succ' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} : iteratedDeriv (n + 1) f = iteratedDeriv n (deriv f)

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

theorem AnalyticAt.hasFPowerSeriesAt {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [CharZero 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜} (h : AnalyticAt 𝕜 f x) : HasFPowerSeriesAt f (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) => iteratedDeriv n f x / ↑n.factorial) x