Majority advantage versus best-of win probability

Proved

GameSetMatch.majorityAdv_odd_eq_bestOfWinProb

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

label-aggregationmajority-voteprobabilityrandom-walktennis

For odd $m$ and any real $q$ : $H_m(2q-1)=2\cdot$ bestOfWinProb m q $-1$ .

Preamble

import Definitions.Def_GameSetMatchInternal

Formal statement

namespace GameSetMatch

/-- For odd `m`: `H_m(2q − 1) = 2·bestOfWinProb m q − 1`. -/
theorem majorityAdv_odd_eq_bestOfWinProb (m : ℕ) (hm : Odd m) (q : ℝ) :
    majorityAdv m (2 * q - 1) = 2 * bestOfWinProb m q - 1 := 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