Lemma 2, strict for interior r

Proved

GameSetMatch.winLossAdv_nested_lt

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

label-aggregationmajority-voteprobabilityrandom-walktennis

Strict for $M>1$ , $n\ge1$ , $0<r<1$ , $0<x\le1$ .

Preamble

import Definitions.Def_GameSetMatchInternal

Formal statement

namespace GameSetMatch

/-- Lemma 2, strict for `0 < r < 1`, `M > 1`, `x > 0`, `n ≥ 1`. -/
theorem winLossAdv_nested_lt (r x : ℝ) (M n : ℕ) (hM : Odd M) (hM1 : 1 < M) (hn : 1 ≤ n)
    (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