Tie-probability formula

Proved

GameSetMatch.tieProb_eq_tilt

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

label-aggregationmajority-voteprobabilityrandom-walktennis

For $0<r\le1/2$ , $x\in[0,1]$ : $Z_J(r,x)=A(x)^J R_J(\rho(x))$ with $A(x)=1-r+r\sqrt{1-x^2}$ , $\rho(x)=r\sqrt{1-x^2}/A(x)$ (equation (28)).

Preamble

import Definitions.Def_GameSetMatchInternal

Formal statement

namespace GameSetMatch

/-- Tie-probability formula (28). -/
theorem tieProb_eq_tilt (r x : ℝ) (J : ℕ) (hr0 : 0 < r) (hr : r ≤ 1 / 2) (hx0 : 0 ≤ x) (hx1 : x ≤ 1) :
    tieProb (scoreContribLaw r x) J
      = (1 - r + r * Real.sqrt (1 - x ^ 2)) ^ J *
        tieIntegral J (r * Real.sqrt (1 - x ^ 2) / (1 - r + r * Real.sqrt (1 - x ^ 2))) := by
  sorry

end GameSetMatch

Source

four_part_nested_best_of_proof.md, Section 5 (Lemma 3); independent_case_full_proof.md, Section 5

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