Advantage of a nested best-of

Proved

GameSetMatch.nestedBestOfWinProb_adv

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

label-aggregationmajority-voteprobabilityrandom-walktennis

For odd set sizes: $2\cdot$ nestedBestOfWinProb ms q $-1=H_{m_1}(H_{m_2}(\cdots H_{m_k}(2q-1)))$ .

Preamble

import Definitions.Def_GameSetMatchInternal

Formal statement

namespace GameSetMatch

/-- Advantage of a nested best-of: `2·nestedBestOfWinProb ms q − 1` is the iterated majority
advantage of `2q − 1`. -/
theorem nestedBestOfWinProb_adv (ms : List ℕ) (hms : ∀ m ∈ ms, Odd m) (q : ℝ) :
    2 * nestedBestOfWinProb ms q - 1 = ms.foldr (fun m x => majorityAdv m x) (2 * 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