Tie integral decreases in the number of contributions

Proved

GameSetMatch.tieIntegral_antitone_left

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

label-aggregationmajority-voteprobabilityrandom-walktennis

For $0\le t\le1/2$ and $I\le J$ : $R_J(t)\le R_I(t)$ .

Preamble

import Definitions.Def_GameSetMatchInternal

Formal statement

namespace GameSetMatch

/-- `R_J(t)` is nonincreasing in `J` for `t ≤ 1/2`. -/
theorem tieIntegral_antitone_left {t : ℝ} (ht0 : 0 ≤ t) (ht : t ≤ 1 / 2) {I J : ℕ} (h : I ≤ J) :
    tieIntegral J t ≤ tieIntegral I 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