Conditioning on the number of counted contributions

Proved

GameSetMatch.winLossAdv_eq_bernstein

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

label-aggregationmajority-voteprobabilityrandom-walktennis

$T_J(r,x)=\sum_{i=0}^J\binom Ji r^i(1-r)^{J-i}H_i(x)$ (equation (13)).

Preamble

import Definitions.Def_GameSetMatchInternal

Formal statement

namespace GameSetMatch

/-- Condition on the number of contributions not ignored. -/
theorem winLossAdv_eq_bernstein (r x : ℝ) (J : ℕ) :
    winLossAdv r x J = ∑ i ∈ Finset.range (J + 1),
      (J.choose i : ℝ) * r ^ i * (1 - r) ^ (J - i) * 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