The coefficient inequality

Proved

GameSetMatch.coeff_ineq

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

label-aggregationmajority-voteprobabilityrandom-walktennis

For odd $M$ , $i\le Mn$ , $x\in[0,1]$ : $\mathbb E H_{L_i}(H_M(x))\le H_i(x)$ (equation (16)).

Preamble

import Definitions.Def_GameSetMatchInternal

Formal statement

namespace GameSetMatch

/-- The coefficient inequality (16). -/
theorem coeff_ineq (M n i : ℕ) (hM : Odd M) (hi : i ≤ M * n) (x : ℝ) (hx0 : 0 ≤ x) (hx1 : x ≤ 1) :
    ∑ l ∈ Finset.range (n + 1), hypergeomWeight M n i l * majorityAdv l (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