Scalar formal multilinear series

This file computes the formal composition of two scalar series in an arbitrary algebra. The algebra need not be commutative: variables retain their original order inside every composition block. It also identifies the iterated derivatives at zero of a convergent complex scalar series.

theorem FormalMultilinearSeries.ofScalars_comp_ofScalars {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [Ring E] [Algebra 𝕜 E] [TopologicalSpace E] [IsTopologicalRing E] (c d : ℕ → 𝕜) : (ofScalars E c).comp (ofScalars E d) = ofScalars E fun (n : ℕ) => ∑ p : Composition n, c p.length * ∏ i : Fin p.length, d (p.blocksFun i)

Composing two scalar formal multilinear series gives the scalar series whose coefficients are obtained by summing over compositions. This remains valid for noncommutative target algebras.

theorem FormalMultilinearSeries.iteratedDeriv_ofScalarsSum_zero (c : ℕ → ℂ) (hc : 0 < (ofScalars ℂ c).radius) (n : ℕ) : iteratedDeriv n (ofScalarsSum c) 0 = ↑n.factorial * c n

The iterated derivatives at zero of the sum of a complex scalar formal multilinear series recover its coefficients, up to the factorial normalization.