Central-binomial series for the majority advantage

Proved

GameSetMatch.majorityAdv_eq_centralBinom_sum

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

label-aggregationmajority-voteprobabilityrandom-walktennis

$H_j(x)=\sum_{i<\lceil j/2\rceil}\binom{2i}{i}4^{-i}x(1-x^2)^i$ .

Preamble

import Definitions.Def_GameSetMatchInternal

Formal statement

namespace GameSetMatch

/-- Closed form; `(j+1)/2 = ⌈j/2⌉`. -/
theorem majorityAdv_eq_centralBinom_sum (j : ℕ) (x : ℝ) :
    majorityAdv j x = ∑ i ∈ Finset.range ((j + 1) / 2),
      ((Nat.centralBinom i : ℝ) / 4 ^ i) * x * (1 - x ^ 2) ^ i := by
  sorry

end GameSetMatch

Source

four_part_nested_best_of_proof.md (private notes, 3 Sep 2026)

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