Continuity of the Faà di Bruno composition #
The m-th coefficient of q.taylorComp p is a finite sum, over the ordered partitions of m,
of continuous multilinear expressions in the coefficients of q and p of order at most m.
So it depends continuously on these finitely many coefficients. Combined with Mathlib's Faà di
Bruno formula iteratedFDerivWithin_comp, this says that the m-th derivative of a composite
g ∘ f depends continuously on the derivatives of g and of f of order at most m, which is
how continuity of composition in C^n topologies is proved.
theorem
Filter.Tendsto.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 : ℕ}
(hq : ∀ k ≤ m, Tendsto (fun (a : α) => q a k) l (nhds (q₀ k)))
(hp : ∀ k ≤ m, Tendsto (fun (a : α) => p a k) l (nhds (p₀ k)))
:
Tendsto (fun (a : α) => (q a).taylorComp (p a) m) l (nhds (q₀.taylorComp p₀ m))
The m-th coefficient of the Taylor composition q.taylorComp p is continuous in the
coefficients of q and of p of order at most m.