Lagrange inversion theorem

TheoremHermite's diagonal form of Lagrange inversion without side conditions#✓fully proved

Let \(R\) be a commutative ring, let \(F\), \(\varphi\), \(w\) and \(G\) be formal power series over \(R\), and write \([X^n]H\) for the coefficient of \(X^n\) in a power series \(H\). Write \(\varphi'\) for the formal derivative of \(\varphi\), and \(\varphi(w)\), \(\varphi'(w)\), \(F(w)\) for the substitution of \(w\) into \(\varphi\), \(\varphi'\), \(F\). If \(w = X\,\varphi(w)\) and \((1 - X\,\varphi'(w))\,G = F(w)\), then \([X^n](F\varphi^n) = [X^n]G\) for every natural number \(n\).

The constant term of \(w\) vanishes automatically, and \(\varphi\) may have zero constant term.

theorem coeff_mul_pow_eq_coeff_of_eq_X_mul_subst {R : Type*} [CommRing R] (n : ℕ)
    {F phi w G : PowerSeries R} (hw : w = PowerSeries.X * phi.subst w)
    (hG : (1 - PowerSeries.X * (PowerSeries.derivative phi).subst w) * G = F.subst w) :
    (PowerSeries.coeff n) (F * phi ^ n) = (PowerSeries.coeff n) G

TheoremHermite's diagonal form of Lagrange inversion#✓fully proved

Let \(R\) be a commutative ring, let \(F\), \(\varphi\), \(w\) and \(G\) be formal power series over \(R\), and write \([X^n]H\) for the coefficient of \(X^n\) in a power series \(H\). Write \(\varphi'\) for the formal derivative of \(\varphi\), and \(\varphi(w)\), \(\varphi'(w)\), \(F(w)\) for the substitution of \(w\) into \(\varphi\), \(\varphi'\), \(F\). Suppose that \(w\) has constant term \(0\), that \(\varphi\) has nonzero constant term, that \(w = X\,\varphi(w)\), and that \((1 - X\,\varphi'(w))\,G = F(w)\). Then \([X^n](F\varphi^n) = [X^n]G\) for every natural number \(n\).

In contrast to the derivative-coefficient form of the Lagrange–Bürmann formula, the derivative here is absorbed into the defining equation for \(G\).

Reference: Bakir Farhi, "Some Applications of the Lagrange Inversion Formula for the k-Fibonacci Numbers", Journal of Integer Sequences 27 (2024), Hermite corollary and derivation lines 205-240.

theorem hermite_lagrange_diagonal_formula
  (n : ℕ) (R : Type*) [CommRing R] (F phi w : PowerSeries R)
  (hw0 : PowerSeries.constantCoeff w = 0)
  (hphi : PowerSeries.coeff 0 phi ≠ 0)
  (hw : w = PowerSeries.X * phi.subst w)
  (G : PowerSeries R)
  (hG : (1 - PowerSeries.X * (PowerSeries.derivative phi).subst w) * G = F.subst w) :
  (PowerSeries.coeff n) (F * phi ^ n) = (PowerSeries.coeff n) G

Sources

• https://cs.uwaterloo.ca/journals/JIS/VOL27/Farhi/farhi35.tex, statement lines 205-210; lines 205-240.

TheoremHermite's form of Lagrange inversion as a series identity#✓fully proved

Let \(\varphi\), \(g\), \(F\) and \(\psi\) be formal power series over \(\mathbb{C}\), write \(F'\) for the formal derivative of \(F\), and write \(h(k)\) for the substitution of a power series \(k\) into a power series \(h\). Suppose that \(\varphi\) has nonzero constant term, that \(F\varphi = X\), and that \(\psi\) is a two-sided compositional inverse of \(F\), that is, \(F(\psi) = X\) and \(\psi(F) = X\). Let \(H = \sum_{n \ge 0} c_n X^n\), where \(c_n\) is the coefficient of \(X^n\) in \(g\varphi^n\). Then

\[X\, g(\psi) = H\, \psi\, F'(\psi).\]

The source states this, with \(F = X/\varphi\), as \(X\, g(\psi) / (\psi\, F'(\psi)) = H\); the form here is cleared of denominators.

theorem hermite_lagrange_inversion
    (φ g F ψ : PowerSeries ℂ)
    (hφ : PowerSeries.coeff 0 φ ≠ 0)
    (hF : F * φ = PowerSeries.X)
    (hpsi1 : PowerSeries.subst ψ F = PowerSeries.X)
    (hpsi2 : PowerSeries.subst F ψ = PowerSeries.X) :
    PowerSeries.X * PowerSeries.subst ψ g =
      (PowerSeries.mk (fun n : ℕ => PowerSeries.coeff n (g * φ ^ n)) :
        PowerSeries ℂ) * ψ *
        PowerSeries.subst ψ (PowerSeries.derivative F)

Sources

• Bakir Farhi, "Some Applications of the Lagrange Inversion Formula for the k-Fibonacci Numbers," Journal of Integer Sequences 27 (2024), Article 24.1.1, Corollary (Hermite, label t-her), lines 205–210, https://cs.uwaterloo.ca/journals/JIS/VOL27/Farhi/farhi35.tex

TheoremLagrange–Bürmann formula from the fixed-point equation alone#✓fully proved

Let \(R\) be a commutative ring and let \(A\), \(\varphi\) and \(g\) be formal power series over \(R\) with \(A = X\,\varphi(A)\), where \(\varphi(A)\) and \(g(A)\) denote the substitution of \(A\) into \(\varphi\) and \(g\). Write \([X^m]H\) for the coefficient of \(X^m\) in a power series \(H\) and \(g'\) for the formal derivative of \(g\). Then for every natural number \(n \ge 1\),

\[n\, [X^n]\, g(A) = [X^{n-1}]\left(g' \varphi^n\right).\]

No condition on the constant term of \(\varphi\) is needed.

theorem fps_lagrange_burmann_coeff' {R : Type*} [CommRing R] (A phi g : PowerSeries R)
    (hfix : A = PowerSeries.X * PowerSeries.subst A phi) (n : ℕ) (hn : 0 < n) :
    (n : R) * PowerSeries.coeff n (PowerSeries.subst A g) =
      PowerSeries.coeff (n - 1) (PowerSeries.derivative g * phi ^ n)

Used by 2

Used byCentral coefficients of Bell matrices · Lagrange–Bürmann formula, coefficient form

TheoremLagrange–Bürmann formula, coefficient form#✓fully proved

Let \(R\) be a commutative ring and let \(A\), \(\varphi\) and \(g\) be formal power series over \(R\) such that the constant term of \(A\) is nilpotent, \(\varphi\) has nonzero constant term, and \(A = X\,\varphi(A)\), where \(\varphi(A)\) and \(g(A)\) denote the substitution of \(A\) into \(\varphi\) and \(g\). Write \([X^m]H\) for the coefficient of \(X^m\) in a power series \(H\) and \(g'\) for the formal derivative of \(g\). Then for every natural number \(n \ge 1\),

\[n\, [X^n]\, g(A) = [X^{n-1}]\left(g' \varphi^n\right).\]

This is the division-free form over a commutative ring: no division by \(n\) is required.

theorem fps_lagrange_burmann_coeff {R : Type*} [CommRing R] (A phi g : PowerSeries R)
    (hsubst : PowerSeries.HasSubst A) (hphi : PowerSeries.coeff 0 phi ≠ 0)
    (hfix : A = PowerSeries.X * PowerSeries.subst A phi) (n : ℕ) (hn : 0 < n) :
    (n : R) * PowerSeries.coeff n (PowerSeries.subst A g) =
      PowerSeries.coeff (n - 1) (PowerSeries.derivative g * phi ^ n)

Sources

• Alexander M. Haupt, "Enumeration of S-omino Towers and Row-Convex k-omino Towers," JIS 24 (2021), proposition at lines 400–407, https://cs.uwaterloo.ca/journals/JIS/VOL24/Haupt/haupt4.tex. Corroborating power specialization: Dmitry Kruchinin and Vladimir Kruchinin, "A Method for Obtaining Generating Functions for Central Coefficients of Triangles," JIS 15 (2012), lines 199–210, https://cs.uwaterloo.ca/journals/JIS/VOL15/Kruchinin/kruchinin5.tex.

Uses 1

Proof usesLagrange–Bürmann formula from the fixed-point equation alone

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.