Prove2Me

Score contributions, win-loss advantages, hypergeometric weights, and the tie integral

Definition
GameSetMatchInternal

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

label-aggregationmajority-voteprobabilityrandom-walktennis

Auxiliary objects used only inside milestone statements.

  • scoreContribLaw r x: one score contribution with win-loss advantage xx, ignored with probability 1−r1-r: +1+1 w.p. r(1+x)/2r(1+x)/2, −1-1 w.p. r(1−x)/2r(1-x)/2, 00 w.p. 1−r1-r.
  • winLossAdv r x J =TJ(r,x)=T_J(r,x): the expected sign of the match-score difference after JJ such contributions (our win-loss advantage with a fair coin on ties).
  • majorityAdv j x =Hj(x)=H_j(x): our win-loss advantage in a best-of-jj when our advantage on each underlying unit is xx; a tie contributes 00.
  • hypergeomWeight M n i l: the probability that a uniformly random ii-subset of MnMn positions meets a fixed nn-subset in exactly ll positions.
  • tieIntegral J t =RJ(t)=12π∫02π(1−t+tcos⁡θ)J dθ=R_J(t)=\frac1{2\pi}\int_0^{2\pi}(1-t+t\cos\theta)^J\,d\theta: the probability that JJ independent contributions equal to +1,−1,0+1,-1,0 with probabilities t/2,t/2,1−tt/2,t/2,1-t sum to zero.
Definition code
import Definitions.Def_GameSetMatch

/-! Internal objects used only inside milestones. Not on the human audit surface. -/

namespace GameSetMatch

/-- Law of one score contribution with win-loss advantage `x`, ignored with probability
`1 − r`: `+1` w.p. `r(1+x)/2`, `−1` w.p. `r(1−x)/2`, `0` w.p. `1 − r`. -/
noncomputable def scoreContribLaw (r x : ℝ) : ℤ → ℝ := fun z =>
  if z = 1 then r * (1 + x) / 2
  else if z = -1 then r * (1 - x) / 2
  else if z = 0 then 1 - r
  else 0

/-- `T_J(r, x)`: our win-loss advantage (expected sign of the match-score difference) after `J`
independent score contributions of law `scoreContribLaw r x`. -/
noncomputable def winLossAdv (r x : ℝ) (J : ℕ) : ℝ :=
  ∑ z ∈ Finset.Icc (-(J : ℤ)) (J : ℤ),
    (if 0 < z then (1 : ℝ) else if z < 0 then -1 else 0) * matchScoreLaw (scoreContribLaw r x) J z

/-- `H_j(x)`: our win-loss advantage in a best-of-`j` when our advantage on each underlying unit
is `x`; a tie contributes `0`. -/
noncomputable def majorityAdv (j : ℕ) (x : ℝ) : ℝ :=
  ∑ i ∈ Finset.range (j + 1),
    (j.choose i : ℝ) * ((1 + x) / 2) ^ i * ((1 - x) / 2) ^ (j - i) *
      (if j < 2 * i then (1 : ℝ) else if 2 * i < j then -1 else 0)

/-- Hypergeometric weight: a uniform `i`-subset of `M·n` positions meets a fixed `n`-subset in
exactly `l` positions. -/
noncomputable def hypergeomWeight (M n i l : ℕ) : ℝ :=
  if l ≤ i then
    (n.choose l : ℝ) * ((M * n - n).choose (i - l) : ℝ) / ((M * n).choose i : ℝ)
  else 0

/-- `R_J(t) = (1/2π) ∫₀^{2π} (1 − t + t·cos θ)^J dθ`: the probability that `J` independent
score contributions equal to `+1, −1, 0` with probabilities `t/2, t/2, 1−t` sum to zero. -/
noncomputable def tieIntegral (J : ℕ) (t : ℝ) : ℝ :=
  (1 / (2 * Real.pi)) * ∫ θ in (0 : ℝ)..(2 * Real.pi), (1 - t + t * Real.cos θ) ^ J

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