Tie integral is positive

Proved

GameSetMatch.tieIntegral_pos

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

label-aggregationmajority-voteprobabilityrandom-walktennis

$R_J(t)>0$ for $0\le t\le1/2$ .

Preamble

import Definitions.Def_GameSetMatchInternal

Formal statement

namespace GameSetMatch

/-- `R_J(t) > 0` for `t ≤ 1/2`. -/
theorem tieIntegral_pos (J : ℕ) {t : ℝ} (ht0 : 0 ≤ t) (ht : t ≤ 1 / 2) : 0 < tieIntegral J t := 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