Formal power series

Rings of formal power series in one or several variables and Hahn series, with formal exponentials, derivatives, coefficient operators and Lagrange inversion.

• Exponential of multivariate formal power series
• Exponentials of coefficient operators
• Hahn series
• Ideals of multivariate power series rings
• Kaluza's theorem on reciprocal power series
• Lagrange inversion theorem
• Partial derivatives of multivariate power series

TheoremTaylor's formula for formal power series#✓fully proved

Let \(R\) be a commutative \(\mathbb{Q}\)-algebra and \(f\) a formal power series over \(R\), with \(j\)-th formal derivative \(f^{(j)}\), and write \([X^i]h\) for the coefficient of \(X^i\) in a power series \(h\). In the ring of formal power series over \(R\) in two variables \(t\) and \(u\),

\[\sum_{i, j \ge 0} \frac{1}{j!}\, [X^i] f^{(j)}\; t^i u^j = f(t + u),\]

where \(f(t + u)\) is the substitution of \(t + u\) into \(f\). In other words, the exponential generating series \(\sum_j f^{(j)}(t)\, u^j / j!\) of the successive derivatives of \(f\) is \(f(t + u)\).

theorem taylorFormula {R : Type*} [CommRing R] [Algebra ℚ R]
    (f : PowerSeries R) :
    (fun d : Fin 2 →₀ ℕ =>
      ((d 1).factorial : ℚ)⁻¹ •
        coeff (d 0) (d⁄dX^[d 1] f)) =
      MvPowerSeries.subst
        (fun _ : Unit =>
          MvPowerSeries.X (0 : Fin 2) + MvPowerSeries.X (1 : Fin 2)) f

Sources

• Emanuele Munarini, Combinatorial Identities for the Tricomi Polynomials, Journal of Integer Sequences 23 (2020), Article 20.9.4, equation (5.32).

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.