Catalan's constant

DefinitionCatalan's constant#✓fully proved

Catalan's constant is the real number \(G = \sum_{n=0}^{\infty} \frac{(-1)^n}{(2n+1)^2}\).

noncomputable def catalanConstant : ℝ :=
  ∑' n : ℕ, (-1 : ℝ) ^ n / (2 * (n : ℝ) + 1) ^ 2

Used by 2

Used byCatalan's constant as a series · The series for Catalan's constant converges to it

TheoremThe series for Catalan's constant converges absolutely#✓fully proved

The series \(\sum_{n=0}^{\infty} \frac{(-1)^n}{(2n+1)^2}\) converges absolutely: its terms are bounded in absolute value by \(\frac{1}{(n+1)^2}\), and \(\sum_{n=0}^{\infty} \frac{1}{(n+1)^2}\) converges.

theorem summable_catalanConstant_terms :
    Summable (fun n : ℕ => (-1 : ℝ) ^ n / (2 * (n : ℝ) + 1) ^ 2)

Used by 1

Used byThe series for Catalan's constant converges to it

TheoremCatalan's constant as a series#✓fully proved

Catalan's constant \(G\) equals \(\sum_{n=0}^{\infty} \frac{(-1)^n}{(2n+1)^2}\).

theorem catalanConstant_eq_tsum :
    catalanConstant = ∑' n : ℕ, (-1 : ℝ) ^ n / (2 * (n : ℝ) + 1) ^ 2

Uses 1

Statement usesCatalan's constant

TheoremThe series for Catalan's constant converges to it#✓fully proved

The series \(\sum_{n=0}^{\infty} \frac{(-1)^n}{(2n+1)^2}\) converges unconditionally, and its sum is Catalan's constant \(G\).

theorem hasSum_catalanConstant :
    HasSum (fun n : ℕ => (-1 : ℝ) ^ n / (2 * (n : ℝ) + 1) ^ 2)
      catalanConstant

Uses 2

Statement usesCatalan's constant

Proof usesThe series for Catalan's constant converges absolutely

TheoremInfinite products for exponentials of Catalan's constant#✓fully proved

Let \(G\) be the sum of the series \(\sum_{n \ge 0} (-1)^n / (2n+1)^2\) (Catalan's constant). Then, as \(m \to \infty\),

\[ \prod_{n=1}^{2m} \left(1 - \frac{2}{2n+1}\right)^{n(-1)^n} \to e^{2G/\pi - 1/2}, \]

\[ \prod_{n=1}^{2m+1} \left(1 - \frac{2}{2n+1}\right)^{n(-1)^n} \to e^{2G/\pi + 1/2}, \]

and

\[ \left(\frac{\prod_{k=0}^{m-1} (4k+3)^{4k+3}}{\prod_{k=0}^{m-1} (4k+1)^{4k+1}}\right)^2 \frac{(4m+3)^{2m+1}}{(4m+1)^{6m+1}} \to e^{4G/\pi}. \]

The products \(\prod_{k=0}^{m-1} (4k+3)^{4k+3}\) and \(\prod_{k=0}^{m-1} (4k+1)^{4k+1}\) are the source's \(3^3 \cdot 7^7 \cdots (4m-1)^{4m-1}\) and \(1^1 \cdot 5^5 \cdots (4m-3)^{4m-3}\).

Proof: Following Kachi and Tzermias, Proposition (catalan), dominated convergence reduces the product limit to the cosecant integral. The substitutions \(x = \pi u/2\) and \(x = 2 \arctan t\), followed by the arctangent power series, evaluate it in terms of \(G\).

public theorem catalan_constant_product_formulas
    (G : ℝ) (hG : HasSum (fun n : ℕ => (-1 : ℝ) ^ n / ((2 * (n : ℝ) + 1) ^ 2)) G) :
    (Filter.Tendsto (fun m : ℕ => ∏ n ∈ Finset.Icc 1 (2 * m),
        (1 - 2 / (2 * (n : ℝ) + 1)) ^ ((n : ℤ) * (-1 : ℤ) ^ n))
      Filter.atTop (nhds (Real.exp (2 * G / Real.pi - 1 / 2)))) ∧
    (Filter.Tendsto (fun m : ℕ => ∏ n ∈ Finset.Icc 1 (2 * m + 1),
        (1 - 2 / (2 * (n : ℝ) + 1)) ^ ((n : ℤ) * (-1 : ℤ) ^ n))
      Filter.atTop (nhds (Real.exp (2 * G / Real.pi + 1 / 2)))) ∧
    Filter.Tendsto (fun m : ℕ =>
        ((∏ k ∈ Finset.range m, (4 * (k : ℝ) + 3) ^ (4 * k + 3)) /
          (∏ k ∈ Finset.range m, (4 * (k : ℝ) + 1) ^ (4 * k + 1))) ^ 2 *
        (4 * (m : ℝ) + 3) ^ (2 * m + 1) / (4 * (m : ℝ) + 1) ^ (6 * m + 1))
      Filter.atTop (nhds (Real.exp (4 * G / Real.pi)))

Sources

• Yasuyuki Kachi and Pavlos Tzermias, "Infinite Products Involving ζ(3) and Catalan's Constant," Journal of Integer Sequences 15 (2012), Article 12.9.4, Proposition, equations, lines 147–165, https://cs.uwaterloo.ca/journals/JIS/VOL15/Tzermias/tzermias2.tex

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.