Tie integral decreases in the step rate

Proved

GameSetMatch.tieIntegral_antitone_right

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

label-aggregationmajority-voteprobabilityrandom-walktennis

For $0\le t\le u\le1/2$ : $R_J(u)\le R_J(t)$ .

Preamble

import Definitions.Def_GameSetMatchInternal

Formal statement

namespace GameSetMatch

/-- `R_J(t)` is nonincreasing in `t` on `[0, 1/2]`. -/
theorem tieIntegral_antitone_right (J : ℕ) {t u : ℝ} (ht0 : 0 ≤ t) (htu : t ≤ u) (hu : u ≤ 1 / 2) :
    tieIntegral J u ≤ 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