Series for π, ζ(3) and other constants

Series and infinite products evaluating constants: π, Catalan's constant, Euler's constant, √2, ζ(3), reciprocal central binomial sums.

TheoremCatalan's product for \(\sqrt{2}\)#✓fully proved

The infinite product over all natural numbers \(m \ge 0\) of \(\frac{(4m+2)^2}{(4m+1)(4m+3)}\) converges unconditionally to \(\sqrt{2}\); that is, \(\frac{2 \cdot 2}{1 \cdot 3} \cdot \frac{6 \cdot 6}{5 \cdot 7} \cdot \frac{10 \cdot 10}{9 \cdot 11} \cdots = \sqrt{2}\).

public theorem catalan_hasProd_sqrt_two :
    HasProd (fun m : Nat =>
      (((4 * m + 2 : Nat) : Real) ^ 2) /
        (((4 * m + 1 : Nat) : Real) * ((4 * m + 3 : Nat) : Real)))
      (Real.sqrt 2)
Sources

TheoremError bound for the partial sums of the series for \(e\)#●ready to prove

For every integer \(n \ge 1\),

\[0 < e - \sum_{k=0}^{n} \frac{1}{k!} < \frac{1}{n \cdot n!}.\]
public theorem_wanted exp_one_sub_sum_inv_factorial_pos_and_lt (n : ℕ) (hn : 0 < n) :
    0 < Real.exp 1 - (∑ k ∈ Finset.range (n + 1), (1 : ℝ) / (Nat.factorial k)) ∧
    Real.exp 1 - (∑ k ∈ Finset.range (n + 1), (1 : ℝ) / (Nat.factorial k)) <
      (1 : ℝ) / (n * Nat.factorial n)
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Functions of one variable), problem ma_proofbench_l1_73.

TheoremRamanujan's series for Euler's constant#✓fully proved

For \(k \ge 0\) let \(A_k = (3^k - 1)/2\). Then the series

\[S = \sum_{k=0}^{\infty} (k+1) \sum_{j=A_k+1}^{A_{k+1}} \frac{1}{(3j)^3 - 3j}\]

converges, and \(\gamma = \log 2 - 2S\), where \(\gamma\) is Euler's constant.

theorem ramanujan_part1_ch8_entry16_eulerconstantseries :
    let A : ℕ → ℕ := fun k => (3 ^ k - 1) / 2
    let term : ℕ → ℝ := fun k =>
      ((k + 1 : ℕ) : ℝ) *
        ∑ j ∈ Finset.Icc (A k + 1) (A (k + 1)),
          (1 : ℝ) / ((3 * (j : ℝ)) ^ 3 - 3 * (j : ℝ))
    Summable term ∧
      Real.eulerMascheroniConstant = Real.log 2 - 2 * ∑' k : ℕ, term k
Sources
  • Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 8, Entry 16.

TheoremSums of reciprocals of central binomial coefficients#✓fully proved

The following three series converge absolutely, with the stated sums:

\[\sum_{n=1}^{\infty} \frac{1}{n \binom{2n}{n}} = \frac{\pi \sqrt{3}}{9},\]
\[\sum_{n=1}^{\infty} \frac{1}{\binom{2n}{n}} = \frac{1}{3} + \frac{2\pi}{9\sqrt{3}},\]
\[\sum_{n=1}^{\infty} \frac{1}{n^2 \binom{2n}{n}} = \frac{\pi^2}{18}.\]
theorem reciprocal_central_binomial_sums :
    HasSum
        (fun m : ℕ =>
          1 / (((m + 1 : ℕ) : ℝ) * (Nat.choose (2 * (m + 1)) (m + 1) : ℝ)))
        (Real.pi * Real.sqrt 3 / 9) ∧
      HasSum
        (fun m : ℕ => 1 / (Nat.choose (2 * (m + 1)) (m + 1) : ℝ))
        (1 / 3 + 2 * Real.pi / (9 * Real.sqrt 3)) ∧
      HasSum
        (fun m : ℕ =>
          1 /
            ((((m + 1 : ℕ) : ℝ) ^ 2) *
              (Nat.choose (2 * (m + 1)) (m + 1) : ℝ)))
        (Real.pi ^ 2 / 18)
Sources
3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.