The iterated derivative of an analytic function

If a function is analytic, written as f (x + y) = ∑ pₙ (y, ..., y) then its n-th iterated derivative at x is given by (v₁, ..., vₙ) ↦ ∑ pₙ (v_{σ (1)}, ..., v_{σ (n)}) where the sum is over all permutations of {1, ..., n}. In particular, it is symmetric.

This generalizes the result of HasFPowerSeriesOnBall.factorial_smul giving D^n f (v, ..., v) = n! * pₙ (v, ..., v).

Main result

• HasFPowerSeriesOnBall.iteratedFDeriv_eq_sum shows that iteratedFDeriv 𝕜 n f x v = ∑ σ : Perm (Fin n), p n (fun i ↦ v (σ i)), when f has p as power series within the set s on the ball B (x, r).
• ContDiffAt.iteratedFDeriv_comp_perm proves the symmetry of the iterated derivative of an analytic function, in the form iteratedFDeriv 𝕜 n f x (v ∘ σ) = iteratedFDeriv 𝕜 n f x v for any permutation σ of Fin n.

Versions within sets are also given.

Implementation

To prove the formula for the iterated derivative, we decompose an analytic function as the sum of fun y ↦ pₙ (y, ..., y) and the rest. For the former, its iterated derivative follows from the formula for iterated derivatives of multilinear maps (see ContinuousMultilinearMap.iteratedFDeriv_comp_diagonal). For the latter, we show by induction on n that if the n-th term in a power series is zero, then the n-th iterated derivative vanishes (see HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_zero).

All these results are proved assuming additionally that the function is analytic on the relevant set (which does not follow from the fact that the function has a power series, if the target space is not complete). This makes it possible to avoid all completeness assumptions in the final statements. When needed, we give versions of some statements assuming completeness and dropping analyticity, for ease of use.

noncomputable def FormalMultilinearSeries.iteratedFDerivSeries {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (k : ℕ) : FormalMultilinearSeries 𝕜 E (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) => E) F)

Formal multilinear series associated to the iterated derivative, defined by iterating p ↦ p.derivSeries and currying suitably. It is defined so that, if a function has p as a power series, then its iterated derivative of order k has p.iteratedFDerivSeries k as a power series.

Equations

• One or more equations did not get rendered due to their size.
• p.iteratedFDerivSeries 0 = (↑(continuousMultilinearCurryFin0 𝕜 E F).symm.toContinuousLinearEquiv).compFormalMultilinearSeries p

theorem HasFPowerSeriesWithinOnBall.iteratedFDerivWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (h : HasFPowerSeriesWithinOnBall f p s x r) (h' : AnalyticOn 𝕜 f s) (k : ℕ) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) : HasFPowerSeriesWithinOnBall (iteratedFDerivWithin 𝕜 k f s) (p.iteratedFDerivSeries k) s x r

If a function has a power series on a ball, then so do its iterated derivatives.

theorem FormalMultilinearSeries.iteratedFDerivSeries_eq_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {k n : ℕ} (h : p (n + k) = 0) : p.iteratedFDerivSeries k n = 0

theorem HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (h : HasFPowerSeriesWithinOnBall f p s x r) (h' : AnalyticOn 𝕜 f s) (hu : UniqueDiffOn 𝕜 s) (hx : x ∈ s) {n : ℕ} (hn : p n = 0) : iteratedFDerivWithin 𝕜 n f s x = 0

If the n-th term in a power series is zero, then the n-th derivative of the corresponding function vanishes.

theorem ContinuousMultilinearMap.iteratedFDeriv_comp_diagonal {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => E) F) (x : E) (v : Fin n → E) : (iteratedFDeriv 𝕜 n (fun (x : E) => f fun (x_1 : Fin n) => x) x) v = ∑ σ : Equiv.Perm (Fin n), f fun (i : Fin n) => v (σ i)

theorem HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (h : HasFPowerSeriesWithinOnBall f p s x r) (h' : AnalyticOn 𝕜 f s) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) {n : ℕ} (v : Fin n → E) : (iteratedFDerivWithin 𝕜 n f s x) v = ∑ σ : Equiv.Perm (Fin n), (p n) fun (i : Fin n) => v (σ i)

If a function has a power series in a ball, then its n-th iterated derivative is given by (v₁, ..., vₙ) ↦ ∑ pₙ (v_{σ (1)}, ..., v_{σ (n)}) where the sum is over all permutations of {1, ..., n}.

theorem HasFPowerSeriesOnBall.iteratedFDeriv_eq_sum {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (h : HasFPowerSeriesOnBall f p x r) (h' : AnalyticOn 𝕜 f Set.univ) {n : ℕ} (v : Fin n → E) : (iteratedFDeriv 𝕜 n f x) v = ∑ σ : Equiv.Perm (Fin n), (p n) fun (i : Fin n) => v (σ i)

If a function has a power series in a ball, then its n-th iterated derivative is given by (v₁, ..., vₙ) ↦ ∑ pₙ (v_{σ (1)}, ..., v_{σ (n)}) where the sum is over all permutations of {1, ..., n}.

theorem HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_completeSpace {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} [CompleteSpace F] (h : HasFPowerSeriesWithinOnBall f p s x r) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) {n : ℕ} (v : Fin n → E) : (iteratedFDerivWithin 𝕜 n f s x) v = ∑ σ : Equiv.Perm (Fin n), (p n) fun (i : Fin n) => v (σ i)

If a function has a power series in a ball, then its n-th iterated derivative is given by (v₁, ..., vₙ) ↦ ∑ pₙ (v_{σ (1)}, ..., v_{σ (n)}) where the sum is over all permutations of {1, ..., n}.

theorem HasFPowerSeriesOnBall.iteratedFDeriv_eq_sum_of_completeSpace {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} [CompleteSpace F] (h : HasFPowerSeriesOnBall f p x r) {n : ℕ} (v : Fin n → E) : (iteratedFDeriv 𝕜 n f x) v = ∑ σ : Equiv.Perm (Fin n), (p n) fun (i : Fin n) => v (σ i)

If a function has a power series in a ball, then its n-th iterated derivative is given by (v₁, ..., vₙ) ↦ ∑ pₙ (v_{σ (1)}, ..., v_{σ (n)}) where the sum is over all permutations of {1, ..., n}.

theorem AnalyticOn.iteratedFDerivWithin_comp_perm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} {x : E} (h : AnalyticOn 𝕜 f s) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) {n : ℕ} (v : Fin n → E) (σ : Equiv.Perm (Fin n)) : (iteratedFDerivWithin 𝕜 n f s x) (v ∘ ⇑σ) = (iteratedFDerivWithin 𝕜 n f s x) v

The n-th iterated derivative of an analytic function on a set is symmetric.

theorem ContDiffWithinAt.iteratedFDerivWithin_comp_perm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} {x : E} (h : ContDiffWithinAt 𝕜 ⊤ f s x) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) {n : ℕ} (v : Fin n → E) (σ : Equiv.Perm (Fin n)) : (iteratedFDerivWithin 𝕜 n f s x) (v ∘ ⇑σ) = (iteratedFDerivWithin 𝕜 n f s x) v

The n-th iterated derivative of an analytic function on a set is symmetric.

theorem AnalyticOn.iteratedFDeriv_comp_perm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (h : AnalyticOn 𝕜 f Set.univ) {n : ℕ} (v : Fin n → E) (σ : Equiv.Perm (Fin n)) : (iteratedFDeriv 𝕜 n f x) (v ∘ ⇑σ) = (iteratedFDeriv 𝕜 n f x) v

The n-th iterated derivative of an analytic function is symmetric.

theorem ContDiffAt.iteratedFDeriv_comp_perm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (h : ContDiffAt 𝕜 ⊤ f x) {n : ℕ} (v : Fin n → E) (σ : Equiv.Perm (Fin n)) : (iteratedFDeriv 𝕜 n f x) (v ∘ ⇑σ) = (iteratedFDeriv 𝕜 n f x) v

The n-th iterated derivative of an analytic function is symmetric.