Majority advantage is superadditive under scaling

Proved

GameSetMatch.majorityAdv_smul_le

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

label-aggregationmajority-voteprobabilityrandom-walktennis

$\lambda H_m(s)\le H_m(\lambda s)$ for $\lambda,s\in[0,1]$ (equation (24)).

Preamble

import Definitions.Def_GameSetMatchInternal

Formal statement

namespace GameSetMatch

/-- `λ·H_m(s) ≤ H_m(λ s)` for `λ, s ∈ [0,1]`. -/
theorem majorityAdv_smul_le (m : ℕ) (lam s : ℝ)
    (h0 : 0 ≤ lam) (h1 : lam ≤ 1) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) :
    lam * majorityAdv m s ≤ majorityAdv m (lam * s) := 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