Knuth's identity for central binomial coefficients

TheoremKnuth's identity in harmonic-number notation#✓fully proved

Let \(x\) be a real number with \(|x| \le 1/4\). Write \(H_k = \sum_{j=1}^{k} \frac{1}{j}\) for the \(k\)-th harmonic number and \(C_n\) for the \(n\)-th Catalan number. Then the series

\[\sum_{n=1}^{\infty} \binom{2n}{n} \left(H_{2n-1} - H_n\right) \frac{x^n}{n}\]

converges absolutely, and its sum is \(\left(\log \sum_{n=0}^{\infty} C_n x^n\right)^2\).

theorem knuth_catalan_log_sq_canonical (x : ℝ) (hx : |x| ≤ 1 / 4) :
  HasSum
    (fun n : ℕ => (Nat.centralBinom (n + 1) : ℝ) *
      (((harmonic (2 * (n + 1) - 1) : ℚ) : ℝ) - ((harmonic (n + 1) : ℚ) : ℝ)) *
      x ^ (n + 1) / ((n : ℝ) + 1))
    ((Real.log (∑' n : ℕ, (catalan n : ℝ) * x ^ n)) ^ 2)
Used by 1
Used byKnuth's identity for central binomial coefficients and harmonic numbers

TheoremKnuth's identity for central binomial coefficients and harmonic numbers#✓fully proved

Let \(x\) be a real number with \(|x| \le 1/4\), and let \(C_n\) denote the \(n\)-th Catalan number. Then the series

\[\sum_{n=1}^{\infty} \binom{2n}{n} \left(\sum_{j=1}^{2n-1} \frac{1}{j} - \sum_{j=1}^{n} \frac{1}{j}\right) \frac{x^n}{n}\]

converges absolutely, and its sum is \(\left(\log \sum_{n=0}^{\infty} C_n x^n\right)^2\).

theorem knuth_catalan_log_sq (x : ℝ) (hx : |x| ≤ 1 / 4) :
  HasSum
    (fun n : ℕ => (Nat.choose (2 * (n + 1)) (n + 1) : ℝ) *
      ((∑ k ∈ Finset.range (2 * (n + 1) - 1), ((k : ℝ) + 1)⁻¹) -
        (∑ k ∈ Finset.range (n + 1), ((k : ℝ) + 1)⁻¹)) *
      x ^ (n + 1) / ((n : ℝ) + 1))
    ((Real.log (∑' n : ℕ, (catalan n : ℝ) * x ^ n)) ^ 2)
Sources
Uses 1
Proof usesKnuth's identity in harmonic-number notation
2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.