Hypergeometric mean

Proved

GameSetMatch.hypergeomWeight_mean

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

label-aggregationmajority-voteprobabilityrandom-walktennis

$\mathbb E L_i=i/M$ (equation (15)).

Preamble

import Definitions.Def_GameSetMatchInternal

Formal statement

namespace GameSetMatch

/-- Hypergeometric mean `i / M`. -/
theorem hypergeomWeight_mean (M n i : ℕ) (hM : 1 ≤ M) (hi : i ≤ M * n) :
    ∑ l ∈ Finset.range (n + 1), hypergeomWeight M n i l * l = (i : ℝ) / 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