Asymptotic expansion of the Catalan numbers
TheoremBernoulli-polynomial expansion from a logarithmic difference equation#✓fully proved
Let \(\alpha\), \(\beta\) and \(c\) be real numbers and let \((u_n)\) be a real sequence with \(u_n \to 0\) such that, for all sufficiently large \(n\), \(u_{n+1} - u_n = \log(1 + \alpha/(n + c)) - \log(1 + \beta/(n + c)) + (\beta - \alpha) \log(1 + 1/(n + c))\). Let \(B_k(x)\) be the \(k\)-th Bernoulli polynomial and, for \(j \ge 0\), put \(a_j = (-1)^j \left(B_{j+2}(\alpha) - B_{j+2}(\beta)\right) / ((j + 1)(j + 2))\). Then for every natural number \(M\), \((n + c)^M \left(u_n - \sum_{j=0}^{M-1} a_j (n + c)^{-(j+1)}\right) \to 0\) as \(n \to \infty\).
The normalization \(u_n \to 0\) fixes the otherwise undetermined additive constant.
Real.tendsto_pow_mul_sub_bernoulli_sum_of_log_diff · 18 lines
public theorem _root_.Real.tendsto_pow_mul_sub_bernoulli_sum_of_log_diff
{u : ℕ → ℝ} (α β c : ℝ)
(hu : Filter.Tendsto u Filter.atTop (nhds 0))
(hstep : ∀ᶠ n : ℕ in Filter.atTop,
u (n + 1) - u n =
Real.log (1 + α / (n + c : ℝ)) - Real.log (1 + β / (n + c : ℝ)) +
(β - α) * Real.log (1 + 1 / (n + c : ℝ))) :
∀ M : ℕ,
Filter.Tendsto
(fun n : ℕ =>
(n + c : ℝ) ^ M *
(u n - ∑ j ∈ Finset.range M,
(-1 : ℝ) ^ (j + 2) *
(Polynomial.aeval α (Polynomial.bernoulli (j + 2)) -
Polynomial.aeval β (Polynomial.bernoulli (j + 2))) /
((j + 1 : ℕ) * (j + 2 : ℕ)) *
(1 / (n + c : ℝ) ^ (j + 1))))
Filter.atTop (nhds 0)TheoremAll-orders logarithmic expansion of the Catalan numbers at a real shift#✓fully proved
Let \(c\) be a real number, let \(C_n\) be the \(n\)-th Catalan number and \(B_k(x)\) the \(k\)-th Bernoulli polynomial, and for \(j \ge 0\) put \(a_j = (-1)^j \left(B_{j+2}(1/2 - c) - B_{j+2}(2 - c)\right) / ((j + 1)(j + 2))\). Then for every natural number \(M\), \((n + c)^M \left(\log\left(C_n \sqrt{\pi (n + c)^3} / 4^n\right) - \sum_{j=0}^{M-1} a_j (n + c)^{-(j+1)}\right) \to 0\) as \(n \to \infty\).
public theorem _root_.tendsto_pow_mul_log_catalan_sub_bernoulli_sum (c : ℝ) :
∀ M : ℕ,
Filter.Tendsto
(fun n : ℕ =>
(n + c : ℝ) ^ M *
(Real.log ((catalan n : ℝ) *
Real.sqrt (Real.pi * (n + c : ℝ) ^ 3) / (4 : ℝ) ^ n) -
∑ j ∈ Finset.range M,
(-1 : ℝ) ^ (j + 2) *
(Polynomial.aeval (1 / 2 - c) (Polynomial.bernoulli (j + 2)) -
Polynomial.aeval (2 - c) (Polynomial.bernoulli (j + 2))) /
((j + 1 : ℕ) * (j + 2 : ℕ)) *
(1 / (n + c : ℝ) ^ (j + 1))))
Filter.atTop (nhds 0)TheoremStirling-type asymptotic expansions of the Catalan numbers#✓fully proved
Let \(C_n\) be the \(n\)-th Catalan number and \(B_k\) the \(k\)-th Bernoulli number, and let \((E_k)\) be a sequence of integers with \(E_0 = 1\) and \(\sum_{j=0}^{\lfloor n/2 \rfloor} \binom{n}{2j} E_{n-2j} = 0\) for every \(n > 0\) (these are the Euler numbers \(1, 0, -1, 0, 5, \dots\)). For \(k \ge 1\) put \(c_k = (-1)^{k+1} \left((2^{-k} - 2) B_{k+1} - k - 1\right) / (k (k + 1))\) and \(d_k = 2^{-4k-2} (4 - E_{2k}) / k\). Then for every \(m \ge 0\), as \(n \to \infty\), \(\log\left(C_n \, n \sqrt{\pi n} / 4^n\right) = \sum_{k=1}^{m} c_k n^{-k} + o(n^{-m})\) and, writing \(x = n + 3/4\), \(\log\left(C_n \sqrt{\pi x^3} / 4^n\right) = \sum_{k=1}^{m} d_k x^{-2k} + o(x^{-2m})\).
The first coefficient is \(c_1 = -9/8\), matching the classical expansion \(C_n = \frac{4^n}{\sqrt{\pi} \, n^{3/2}} \left(1 - \frac{9}{8n} + \dots\right)\).
Proof: The Catalan recurrence gives a logarithmic first-difference equation. Telescoping its Bernoulli-polynomial expansion yields both all-orders formulas.
MetaMathlibExt.catalan_stirling_asymptotic_expansions · 32 lines
public theorem catalan_stirling_asymptotic_expansions
(E : ℕ → ℤ)
(hE : E 0 = 1 ∧ ∀ n : ℕ, 0 < n →
(∑ j ∈ Finset.range (n / 2 + 1),
(n.choose (2 * j) : ℤ) * E (n - 2 * j)) = 0) :
((∀ m : ℕ,
Filter.Tendsto
(fun n : ℕ =>
(n : ℝ) ^ m *
(Real.log
((catalan n : ℝ) * ((n : ℝ) * Real.sqrt (Real.pi * n)) /
(4 : ℝ) ^ n) -
∑ j ∈ Finset.range m,
(-1 : ℝ) ^ (j + 2) *
((((2 : ℝ) ^ (j + 1))⁻¹ - 2) *
(bernoulli (j + 2) : ℝ) - (j + 1 : ℕ) - 1) /
((j + 1 : ℕ) * (j + 2 : ℕ)) *
(1 / ((n : ℝ) ^ (j + 1)))))
Filter.atTop (nhds 0)) ∧
(∀ m : ℕ,
Filter.Tendsto
(fun n : ℕ =>
(n + 3 / 4 : ℝ) ^ (2 * m) *
(Real.log
((catalan n : ℝ) *
Real.sqrt (Real.pi * (n + 3 / 4 : ℝ) ^ 3) /
(4 : ℝ) ^ n) -
∑ j ∈ Finset.range m,
((2 : ℝ) ^ (4 * (j + 1) + 2))⁻¹ *
(4 - (E (2 * (j + 1)) : ℝ)) / (j + 1 : ℕ) *
(1 / ((n + 3 / 4 : ℝ) ^ (2 * (j + 1))))))
Filter.atTop (nhds 0)))Sources
- Neven Elezović, "Asymptotic Expansions of Central Binomial Coefficients and Catalan Numbers," Journal of Integer Sequences 17 (2014), Article 14.2.1, Catalan Stirling-type theorem (unlabeled, equation 42), lines 626–637, https://cs.uwaterloo.ca/journals/JIS/VOL17/Elezovic/elezovic5.tex
TheoremUniqueness of the even-power shift in Catalan asymptotics#✓fully proved
Let \(C_n = \binom{2n}{n} / (n + 1)\) be the \(n\)-th Catalan number. For a real number \(\alpha\), there is a real sequence \((a_k)_{k \ge 0}\) with \(a_{2k+1} = 0\) for every \(k\) such that, for every \(N \ge 0\), the difference \(C_n \sqrt{\pi} \, (n + \alpha)^{3/2} / 4^n - \sum_{k=0}^{N} a_k (n + \alpha)^{-k}\) is \(o\left((n + \alpha)^{-N}\right)\) as \(n \to \infty\), if and only if \(\alpha = 3/4\).
Elezović phrases this as the expansion "containing only odd terms"; the condition meant is that the odd-indexed coefficients vanish: his displayed series for \(\alpha = 3/4\) has only even powers, and his proof obtains \(\alpha = 3/4\) by setting the first odd coefficient to zero.
Proof: The reverse implication exponentiates the all-orders logarithmic expansion of the Catalan numbers and uses the reflection symmetry of the Bernoulli polynomials to eliminate odd powers. The first logarithmic coefficient gives uniqueness, following Elezović.
MetaMathlibExt.catalan_odd_terms_shift_unique · 15 lines
public theorem catalan_odd_terms_shift_unique :
∀ α : ℝ,
(∃ a : ℕ → ℝ,
(∀ N : ℕ,
Filter.Tendsto
(fun n : ℕ =>
((n : ℝ) + α) ^ N *
(((Nat.choose (2 * n) n : ℝ) / ((n : ℝ) + 1) *
Real.sqrt Real.pi *
Real.rpow ((n : ℝ) + α) ((3 : ℝ) / 2) /
(4 : ℝ) ^ n) -
∑ k ∈ Finset.range (N + 1), a k / ((n : ℝ) + α) ^ k))
Filter.atTop (nhds 0)) ∧
(∀ k : ℕ, a (2 * k + 1) = 0)) ↔
α = (3 : ℝ) / 4Sources
- Neven Elezović, "Asymptotic Expansions of Central Binomial Coefficients and Catalan Numbers," Journal of Integer Sequences 17 (2014), Article 14.2.1, Corollary, lines 568–578, https://cs.uwaterloo.ca/journals/JIS/VOL17/Elezovic/elezovic5.tex
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.