Small samples have more advantage per unit

Proved

GameSetMatch.majorityAdv_ge_ratio

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

label-aggregationmajority-voteprobabilityrandom-walktennis

For odd $M$ , $i\le M$ , $x\in[0,1]$ : $\frac iM H_M(x)\le H_i(x)$ (equation (10)).

Preamble

import Definitions.Def_GameSetMatchInternal

Formal statement

namespace GameSetMatch

/-- Small samples have more advantage per unit: `(i/M)·H_M ≤ H_i` for `i ≤ M`. -/
theorem majorityAdv_ge_ratio (M i : ℕ) (hM : Odd M) (hi : i ≤ M) (x : ℝ) (hx0 : 0 ≤ x) (hx1 : x ≤ 1) :
    (i : ℝ) / M * majorityAdv M x ≤ majorityAdv i 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