Bhattacharyya bound

Proved

GameSetMatch.majorityAdv_sq_le

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

label-aggregationmajority-voteprobabilityrandom-walktennis

For odd $M$ and $x\in[0,1]$ : $H_M(x)^2\le1-(1-x^2)^M$ (equation (31)).

Preamble

import Definitions.Def_GameSetMatchInternal

Formal statement

namespace GameSetMatch

/-- Bhattacharyya bound (31): `H_M(x)² ≤ 1 − (1 − x²)^M`. -/
theorem majorityAdv_sq_le (M : ℕ) (hM : Odd M) (x : ℝ) (hx0 : 0 ≤ x) (hx1 : x ≤ 1) :
    (majorityAdv M x) ^ 2 ≤ 1 - (1 - x ^ 2) ^ M := 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