Lagrange inversion series

TheoremRamanujan's series for powers of a root of \(x = a \log x\) (Entry 13)#✓fully proved

Let \(a\) be a real number with \(|a| \ge e\). Then there is a real number \(x > 0\) with \(x = a \log x\) such that for every real number \(n\) the series

\[1 + \sum_{k=1}^{\infty} \frac{n (n+k)^{k-1}}{a^k\, k!}\]

is summable with sum \(x^n\).

theorem ramanujan_part1_ch3_entry13 (a : ℝ) (ha : |a| ≥ Real.exp 1) :
    ∃ x : ℝ, 0 < x ∧ x = a * Real.log x ∧ ∀ n : ℝ,
      HasSum (fun k : ℕ => if k = 0 then (1 : ℝ) else n * (n + (k : ℝ)) ^ (k - 1) /
          (a ^ k * (Nat.factorial k : ℝ))) (x ^ n)
Sources
  • Berndt, Ramanujan's Notebooks Part I, Chapter 3, definition (12.1), printed p. 66 / PDF p. 76, and Entry 13, printed pp. 69--70 / PDF pp. 79--80; historical attribution on printed p. 72 / PDF p. 82.

TheoremAbel's binomial identity#✓fully proved

For a complex number \(w\), let \(A_0(x) = 1\) and \(A_j(x) = x (x + j w)^{j-1}\) for \(j \ge 1\). Then for all complex numbers \(x\), \(y\) and every natural number \(n\),

\[\sum_{j=0}^{n} \binom{n}{j} A_j(x) A_{n-j}(y) = A_n(x + y).\]
theorem schroder_abel_binomial (w x y : ℂ) (n : ℕ) :
    (∑ j ∈ Finset.range (n + 1), (n.choose j : ℂ) *
        (if j = 0 then 1 else x * (x + (j : ℂ) * w) ^ (j - 1)) *
        (if n - j = 0 then 1
          else y * (y + ((n - j : ℕ) : ℂ) * w) ^ (n - j - 1))) =
      if n = 0 then 1 else (x + y) * (x + y + (n : ℂ) * w) ^ (n - 1)
Used by 1
Used byHagen–Rothe convolution for Lagrange series coefficients

TheoremSchröder's exponential series#✓fully proved

Let \(z\) and \(w\) be complex numbers with \(|w| \le |e^{w-1}|\) and \(|w| \le 1\). Then the series

\[1 + \sum_{k=1}^{\infty} \frac{z (z + k w)^{k-1} e^{-k w}}{k!}\]

converges unconditionally, and its sum is \(e^z\).

The set of complex numbers \(w\) with \(|w| \le |e^{w-1}|\) has a bounded lobe containing \(0\) and an unbounded lobe, which meet only at \(w = 1\). The condition \(|w| \le 1\) selects the bounded lobe (given the first condition, it is equivalent to \(\operatorname{Re} w \le 1\)); on the unbounded lobe the identity fails in general.

Proof: Following Berndt's formula (13.8), we use Abel's binomial identity, a Cauchy product and a holomorphic ODE; radial continuity selects the unit-disk branch of \(u \mapsto u e^{-u}\).

theorem ramanujan_part1_ch3_entry13_corollary_schroder
    (z w : ℂ) (hw : ‖w‖ ≤ ‖Complex.exp (w - 1)‖) (hw1 : ‖w‖ ≤ 1) :
    HasSum (fun k : ℕ => if k = 0 then 1 else z * (z + (k : ℂ) * w) ^ (k - 1) *
        Complex.exp (-(k : ℂ) * w) / (Nat.factorial k : ℂ)) (Complex.exp z)
Sources
  • Berndt, Ramanujan's Notebooks Part I, Chapter 3, Corollary to Entry 13, formula (13.8), printed p. 70 / PDF p. 80.

TheoremRamanujan's series for powers of the Catalan generating function#✓fully proved

Let \(n\) and \(a\) be real numbers with \(|a| \le 1/4\). For a natural number \(k\) put \(t_k = 0\) if \(k < 2\), and

\[t_k = \frac{a^k}{k!} \prod_{j=k+1}^{2k-1} (n + j)\]

if \(k \ge 2\). Then the series \(\sum_k t_k\) is summable and

\[\left(\frac{2}{1 + \sqrt{1 - 4a}}\right)^{n} = 1 + n a + n \sum_{k=0}^{\infty} t_k.\]
theorem ramanujan_part1_ch3_entry14_cor1_catalanpowerseries
    (n a : ℝ) (ha : |a| ≤ 1 / 4) :
    let term := fun k : ℕ => if k < 2 then 0 else
      (∏ j ∈ Finset.Ico (k + 1) (2 * k), (n + (j : ℝ))) * a ^ k / (Nat.factorial k : ℝ)
    Summable term ∧
      Real.rpow (2 / (1 + Real.sqrt (1 - 4 * a))) n = 1 + n * a + n * ∑' k, term k
Sources
  • Berndt, Ramanujan's Notebooks Part I, Chapter 3, Entry 14, Corollary 1, printed p. 71; scan PDF p. 81.
Uses 1 · Used by 1
Proof usesClosed form of the Catalan generating function
Used byRamanujan's exponential series for powers of two

DefinitionLagrange series coefficients#✓fully proved

For real numbers \(p\), \(q\), \(n\) and a natural number \(k\), the Lagrange series coefficient \(C_{p,q}(n, k)\) is \(1\) if \(k = 0\), and for \(k \ge 1\) it is

\[C_{p,q}(n, k) = n \prod_{j=1}^{k-1} (n + k p - j q)\]

(an empty product when \(k = 1\)).

def lagrangeSeriesCoefficient (p q n : ℝ) (k : ℕ) : ℝ :=
  if k = 0 then 1 else
    n * ∏ j ∈ Finset.range (k - 1), (n + (k : ℝ) * p - ((j + 1 : ℕ) : ℝ) * q)
Used by 4
Used byHagen–Rothe convolution for Lagrange series coefficients · Lagrange series coefficients of positive degree · Lagrange series coefficient of degree zero · Ramanujan's Lagrange series

TheoremLagrange series coefficient of degree zero#✓fully proved

For all real numbers \(p\), \(q\), \(n\), the Lagrange series coefficient \(C_{p,q}(n, 0)\) of degree \(0\) equals \(1\).

@[simp]
theorem lagrangeSeriesCoefficient_zero (p q n : ℝ) :
    lagrangeSeriesCoefficient p q n 0 = 1
Uses 1 · Used by 2
Statement usesLagrange series coefficients
Used byHagen–Rothe convolution for Lagrange series coefficients · Ramanujan's Lagrange series

TheoremLagrange series coefficients of positive degree#✓fully proved

For all real numbers \(p\), \(q\), \(n\) and every natural number \(k \ne 0\), the Lagrange series coefficient of degree \(k\) is

\[C_{p,q}(n, k) = n \prod_{j=1}^{k-1} (n + k p - j q).\]
theorem lagrangeSeriesCoefficient_of_ne_zero (p q n : ℝ) {k : ℕ} (hk : k ≠ 0) :
    lagrangeSeriesCoefficient p q n k =
      n * ∏ j ∈ Finset.range (k - 1),
        (n + (k : ℝ) * p - ((j + 1 : ℕ) : ℝ) * q)
Uses 1 · Used by 2
Statement usesLagrange series coefficients
Used byHagen–Rothe convolution for Lagrange series coefficients · Ramanujan's Lagrange series

TheoremHagen–Rothe convolution for Lagrange series coefficients#✓fully proved

For all real numbers \(p\), \(q\), \(r\), \(s\) and every natural number \(m\), the Lagrange series coefficients \(C_{p,q}\) satisfy

\[C_{p,q}(r + s, m) = \sum_{k=0}^{m} \binom{m}{k} C_{p,q}(r, k) \, C_{p,q}(s, m - k).\]
theorem lagrangeSeriesCoefficient_add (p q r s : ℝ) (m : ℕ) :
    lagrangeSeriesCoefficient p q (r + s) m =
      ∑ k ∈ Finset.range (m + 1), (Nat.choose m k : ℝ) *
        lagrangeSeriesCoefficient p q r k * lagrangeSeriesCoefficient p q s (m - k)
Uses 4 · Used by 1
Statement usesLagrange series coefficients
Proof usesAbel's binomial identity · Lagrange series coefficients of positive degree · Lagrange series coefficient of degree zero
Used byRamanujan's Lagrange series

TheoremRamanujan's Lagrange series#✓fully proved

Let \(p > 0\) and \(q > 0\) be real numbers with \(p \ne q\), and let \(a\) be a complex number with \(|a| \le p^{-p/q} |p - q|^{(p - q)/q}\). Then there is a complex number \(L\) with \(a q e^{p L} - e^{q L} + 1 = 0\) such that, for every real number \(n\), the series

\[1 + \sum_{k=1}^{\infty} \frac{n a^k}{k!} \prod_{j=1}^{k-1} (n + k p - j q)\]

converges unconditionally to \(e^{n L}\).

Proof: The argument uses the Hagen--Rothe convolution, a Stirling-type coefficient bound uniform through the boundary circle, and a continuous exponential lift.

theorem ramanujan_part1_ch3_entry14_lagrange_series (p q : ℝ)
    (hp : 0 < p)
        (hq : 0 < q) (hpq : p ≠ q) (a : ℂ) (ha : ‖a‖ ≤ p ^ (-p / q) * |p - q| ^ ((p - q) / q)) :
    ∃ L : ℂ, a * (↑q : ℂ) * Complex.exp (↑p * L) - Complex.exp (↑q * L) + 1 = 0 ∧ ∀ n : ℝ,
        HasSum (fun k : ℕ => if k = 0 then (1 : ℂ) else (↑n : ℂ) *
            Finset.prod (Finset.range (k - 1))
                (fun j => (↑n : ℂ) + (k : ℂ) * (↑p : ℂ) - ((j + 1 : ℂ) * (↑q : ℂ))) * a ^ k /
                    (↑(Nat.factorial k) : ℂ)) (Complex.exp ((↑n : ℂ) * L))
Sources
  • Berndt, Ramanujan's Notebooks Part I, Chapter 3, Entry 14, formulas (14.1)--(14.5), printed pp. 70--71 / PDF pp. 80--81; attribution on printed p. 72 / PDF p. 82.
Uses 5
Proof usesLagrange series coefficients · Hagen–Rothe convolution for Lagrange series coefficients · Lagrange series coefficients of positive degree · Lagrange series coefficient of degree zero · Continuous solutions of the exponential functional equation

TheoremRamanujan's exponential series for powers of two#✓fully proved

Let \(m\) and \(n\) be real numbers with \(0 < n \le 2\). Then the series

\[1 + \sum_{k=1}^{\infty} \frac{m}{2^{k n} \, k!} \prod_{j=1}^{k-1} (m + k n - j)\]

converges unconditionally to \(2^m\).

Proof: Following Berndt and the generalized binomial series of Graham, Knuth, and Patashnik, the series is realized as \(B_n(z)^m\), where \(B_n = 1 + z B_n^n\); root selection at \(z = 2^{-n}\), with the endpoint supplied by Entry 14's Catalan-power series, gives \(B_n = 2\).

theorem ramanujan_part1_ch3_entry15_example1_exponential_series (m n : ℝ)
    (hn_pos : 0 < n) (hn_le : n ≤ 2) :
    HasSum (fun k : ℕ =>
      if k = 0 then (1 : ℝ)
      else (m * ∏ j ∈ Finset.range (k - 1), (m + (k : ℝ) * n - ((j : ℝ) + 1))) /
        ((2 : ℝ) ^ ((k : ℝ) * n) * (Nat.factorial k : ℝ))) ((2 : ℝ) ^ m)
Sources
  • Berndt, Ramanujan's Notebooks Part I, Chapter 3, Entry 15, Example 1, printed pp. 73-75 / PDF pp. 83-85.
Uses 1
Proof usesRamanujan's series for powers of the Catalan generating function

TheoremRamanujan's inverse series for \(u - \log u\)#✓fully proved

There exist a real number \(r > 0\) and real coefficients \(b_0, b_1, b_2, \dots\) with \(b_0 = 1\), \(b_1 = -1\), \(b_2 = 1/3\), \(b_3 = -1/36\) and \(b_4 = -1/270\) such that the power series \(\sum_k b_k x^k\) is summable for every real \(x\) with \(|x| < r\), and for every real \(x\) with \(0 < x < r\) the sum \(u\) of this series satisfies \(0 < u < 1\) and \(u - \log u = 1 + x^2/2\), and the series \(\sum_{j \ge 2} (1 - u)^j / j\) converges unconditionally to \(x^2/2\).

theorem ramanujan_part1_ch3_entry15_inverse_series :
    ∃ (r : ℝ) (b : ℕ → ℝ),
      0 < r ∧ b 0 = 1 ∧ b 1 = -1 ∧ b 2 = (1 : ℝ) / 3 ∧ b 3 = -(1 : ℝ) / 36 ∧
        b 4 = -(1 : ℝ) / 270 ∧
        (∀ x : ℝ, |x| < r → ∃ u : ℝ, HasSum (fun k : ℕ => b k * x ^ k) u) ∧
        ∀ x : ℝ, 0 < x → x < r → ∀ u : ℝ, HasSum (fun k : ℕ => b k * x ^ k) u →
          0 < u ∧ u < 1 ∧ u - Real.log u = 1 + x ^ 2 / 2 ∧
            HasSum (fun j : ℕ => (1 - u) ^ (j + 2) / (↑(j + 2) : ℝ)) (x ^ 2 / 2)
Sources
  • Berndt, Ramanujan's Notebooks Part I, Chapter 3, Entry 15, local inverse-series clause, printed p. 73 / PDF p. 83.

TheoremRamanujan's tree-function series (Chapter 3, Entry 15)#✓fully proved

Let \(x\) and \(u\) be real numbers with \(0 < u < 1\) and \(u - \log u = 1 + x^2/2\). Then the series

\[\sum_{k=0}^{\infty} \frac{(k+1)^{k-1}}{k!}\, e^{-k(1 + x^2/2)}\]

converges to \(u\, e^{1 + x^2/2}\).

theorem ramanujan_part1_ch3_entry15_treeseries (x : ℝ)
    (u : ℝ) (hu_pos : 0 < u) (hu_lt : u < 1)
    (hu_eq : u - Real.log u = 1 + x ^ 2 / 2) :
    HasSum (fun k : ℕ => ((k + 1 : ℝ) ^ (k - 1) / (Nat.factorial k : ℝ)) *
        Real.exp (-(k : ℝ) * (1 + x ^ 2 / 2)))
      (u * Real.exp (1 + x ^ 2 / 2))
Sources
  • Berndt, Ramanujan's Notebooks Part I, Chapter 3, Entry 15, formulas (15.1)-(15.2), printed p. 73; scan PDF p. 83.

TheoremTaylor coefficients of the solution of \(x^x = a^a e^h\) (Chapter 3, Entry 17)#✓fully proved

For every real number \(a > 1/e\) there exist a real number \(R > 0\) and a function \(x : \mathbb{R} \to \mathbb{R}\), analytic at \(0\), with \(x(0) = a\), such that \(x(h) > 0\) and \(x(h)^{x(h)} = a^a e^h\) for all real \(h\) with \(|h| < R\), and such that the numbers \(A_k = (-a)^{k-1} x^{(k)}(0)\) for \(k \ge 1\) satisfy, for every integer \(r \ge 2\),

\[A_r = \frac{(r - 2)\, A_{r-1} + \sum_{k=1}^{r-1} \binom{r-1}{k} A_k A_{r-k}}{1 + \log a}.\]
theorem ramanujan_part1_ch3_entry17 :
    ∀ (a : ℝ), 1 / Real.exp 1 < a →
        ∃ (R : ℝ) (x : ℝ → ℝ), 0 < R ∧ AnalyticAt ℝ x (0 : ℝ) ∧ x 0 = a ∧
            (∀ h : ℝ, |h| < R → 0 < x h ∧ x h ^ x h = a ^ a * Real.exp h) ∧ ∀ r : ℕ, 2 ≤ r →
                (-a) ^ (r - 1) * iteratedDeriv r x 0 = (1 + Real.log a)⁻¹ * ((r : ℝ) - 2) *
                    ((-a) ^ (r - 2) * iteratedDeriv (r - 1) x 0) + (1 + Real.log a)⁻¹ *
                        ∑ k ∈ Finset.Icc 1 (r - 1), (Nat.choose (r - 1) k : ℝ) *
                            ((-a) ^ (k - 1) * iteratedDeriv k x 0) *
                                ((-a) ^ (r - k - 1) * iteratedDeriv (r - k) x 0)
Sources
  • Berndt, Ramanujan's Notebooks Part I, Chapter 3, corrected Entry 17, formulas (17.1)--(17.7), printed pp. 81--83 / PDF pp. 91--93.
13 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.