Lemma 2: homogeneous random-scoring lemma

Proved

GameSetMatch.winLossAdv_nested_le

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

label-aggregationmajority-voteprobabilityrandom-walktennis

For odd $M$ and $r,x\in[0,1]$ : $T_n(r,H_M(x))\le T_{nM}(r,x)$ (equation (6)).

Preamble

import Definitions.Def_GameSetMatchInternal

Formal statement

namespace GameSetMatch

/-- **Lemma 2.** `T_n(r, H_M(x)) ≤ T_{nM}(r, x)` for odd `M`, all `r, x ∈ [0,1]`. -/
theorem winLossAdv_nested_le (r x : ℝ) (M n : ℕ) (hM : Odd M)
    (hr0 : 0 ≤ r) (hr1 : r ≤ 1) (hx0 : 0 ≤ x) (hx1 : x ≤ 1) :
    winLossAdv r (majorityAdv M x) n ≤ winLossAdv r x (n * M) := 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