Fair-coin best-of as a fair-coin match

Proved

GameSetMatch.bestOfFairCoinWinProb_eq

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

label-aggregationmajority-voteprobabilityrandom-walktennis

bestOfFairCoinWinProb N q equals the fair-coin match win probability of $N$ unscored points (law scoredSetLaw 1 0 0 q).

Preamble

import Definitions.Def_GameSetMatchInternal

Formal statement

namespace GameSetMatch

/-- A fair-coin best-of-`N` is the fair-coin match win probability of `N` unscored points. -/
theorem bestOfFairCoinWinProb_eq (N : ℕ) (q : ℝ) :
    bestOfFairCoinWinProb N q = fairCoinWinProb (scoredSetLaw 1 0 0 q) N := by
  sorry

end GameSetMatch

Source

Mission statement 'Don't Label Twice: Game, Set, Match', parts (a)–(d)

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