Majority of all points beats a majority of majorities

Proved

GameSetMatch.majorityAdv_nested_le

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

label-aggregationmajority-voteprobabilityrandom-walktennis

For odd $m$ , $\ell$ and $x\in[0,1]$ : $H_\ell(H_m(x))\le H_{m\ell}(x)$ (equation (12)).

Preamble

import Definitions.Def_GameSetMatchInternal

Formal statement

namespace GameSetMatch

/-- Majority of all points beats a majority of majorities: `H_l(H_m(x)) ≤ H_{m l}(x)`
for odd `m`, `l`. -/
theorem majorityAdv_nested_le (m l : ℕ) (hm : Odd m) (hl : Odd l) (x : ℝ) (hx0 : 0 ≤ x) (hx1 : x ≤ 1) :
    majorityAdv l (majorityAdv m x) ≤ majorityAdv (m * l) x := 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