Wallis integral

Proved

GameSetMatch.centralBinom_div_four_pow_eq_integral

by willma · Sep 4, 2026 · Mathlib c5ea003 (Lean v4.30.0)

label-aggregationmajority-voteprobabilityrandom-walktennis

$\binom{2j}{j}4^{-j}=\frac2\pi\int_0^{\pi/2}\cos^{2j}\theta\,d\theta$ .

Preamble

import Definitions.Def_GameSetMatchInternal

Formal statement

namespace GameSetMatch

/-- Wallis: `C(2j,j)/4^j = (2/π)∫₀^{π/2} cos^{2j}`. -/
theorem centralBinom_div_four_pow_eq_integral (j : ℕ) :
    (Nat.centralBinom j : ℝ) / 4 ^ j
      = (2 / Real.pi) * ∫ θ in (0 : ℝ)..(Real.pi / 2), Real.cos θ ^ (2 * j) := by
  sorry

end GameSetMatch

Source

four_part_nested_best_of_proof.md, Section 5 (Lemma 3); independent_case_full_proof.md, Section 5

Human review

Endorsed by Shuze Chen · Sep 4, 2026
Endorsed by willma · Sep 4, 2026
Confirmed by the mission captain (proposal self-audit).

View graph