Recovering inverse Taylor coefficients

In the Faà di Bruno formula, the partition into singletons is the only term involving the highest coefficient of the outer series. All other terms involve strictly lower outer coefficients. If the linear term of the inner series admits a continuous right inverse, this gives a recursive formula for the outer coefficients from the composite. It also proves their continuous dependence, the algebraic input to continuity of inversion in differentiable map spaces.

We use Mathlib's ordered-partition formulation of the Faà di Bruno formula, rather than power-series composition: the coefficients here represent derivatives without factorials.

@[simp]

theorem OrderedFinpartition.sum_partSize {n : ℕ} (c : OrderedFinpartition n) : ∑ i : Fin c.length, c.partSize i = n

The sizes of the parts of an ordered partition add up to the size of the ground set.

@[simp]

theorem OrderedFinpartition.length_eq_iff {n : ℕ} (c : OrderedFinpartition n) : c.length = n ↔ c = atomic n

A partition has as many parts as elements exactly when it is the singleton partition.

theorem OrderedFinpartition.length_lt_of_ne_atomic {n : ℕ} (c : OrderedFinpartition n) (hc : c ≠ atomic n) : c.length < n

A partition other than the singleton partition has strictly fewer parts than elements.

@[simp]

theorem FormalMultilinearSeries.compAlongOrderedFinpartition_atomic {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (m : ℕ) : q.compAlongOrderedFinpartition p (OrderedFinpartition.atomic m) = (q m).compContinuousLinearMap fun (x : Fin m) => (continuousMultilinearCurryFin1 𝕜 E F) (p 1)

The singleton partition term of Taylor composition precomposes each variable with the linear coefficient of the inner series.

theorem FormalMultilinearSeries.eq_taylorComp_sub_sum_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (m : ℕ) (A : F →L[𝕜] E) (hA : (continuousMultilinearCurryFin1 𝕜 E F) (p 1) ∘SL A = ContinuousLinearMap.id 𝕜 F) : q m = (q.taylorComp p m - ∑ c ∈ Finset.univ.erase (OrderedFinpartition.atomic m), q.compAlongOrderedFinpartition p c).compContinuousLinearMap fun (x : Fin m) => A

Recover the highest outer Taylor coefficient from the composite and the lower outer coefficients, using a right inverse of the inner linear coefficient.

theorem TauCeti.tendsto_apply_zero_of_taylorComp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {α : Type u_5} {l : Filter α} {q : α → FormalMultilinearSeries 𝕜 F G} {p : α → FormalMultilinearSeries 𝕜 E F} {q₀ : FormalMultilinearSeries 𝕜 F G} {p₀ : FormalMultilinearSeries 𝕜 E F} (hcomp : Filter.Tendsto (fun (a : α) => (q a).taylorComp (p a) 0) l (nhds (q₀.taylorComp p₀ 0))) : Filter.Tendsto (fun (a : α) => q a 0) l (nhds (q₀ 0))

The zeroth outer Taylor coefficient converges whenever the zeroth composite coefficient converges, without any assumption on the inner series or an inverse of its linear term.

theorem Filter.Tendsto.of_taylorComp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {α : Type u_5} {l : Filter α} {q : α → FormalMultilinearSeries 𝕜 F G} {p : α → FormalMultilinearSeries 𝕜 E F} {q₀ : FormalMultilinearSeries 𝕜 F G} {p₀ : FormalMultilinearSeries 𝕜 E F} {m : ℕ} {A : α → F →L[𝕜] E} {A₀ : F →L[𝕜] E} (hm : 0 < m) (hq : ∀ (k : ℕ), 0 < k → k < m → Tendsto (fun (a : α) => q a k) l (nhds (q₀ k))) (hp : ∀ (k : ℕ), 0 < k → k ≤ m → Tendsto (fun (a : α) => p a k) l (nhds (p₀ k))) (hcomp : Tendsto (fun (a : α) => (q a).taylorComp (p a) m) l (nhds (q₀.taylorComp p₀ m))) (hA : Tendsto A l (nhds A₀)) (hAp : ∀ᶠ (a : α) in l, (continuousMultilinearCurryFin1 𝕜 E F) (p a 1) ∘SL A a = ContinuousLinearMap.id 𝕜 F) (hA₀ : (continuousMultilinearCurryFin1 𝕜 E F) (p₀ 1) ∘SL A₀ = ContinuousLinearMap.id 𝕜 F) : Tendsto (fun (a : α) => q a m) l (nhds (q₀ m))

A positive-order Taylor coefficient of the outer series converges if the composite coefficient, the positive lower outer coefficients, the positive inner coefficients up to that order, and a right inverse of the inner linear coefficient converge.