Bernstein degree elevation
ProvedGameSetMatch.bernstein_elevatelabel-aggregationmajority-voteprobabilityrandom-walktennis
Equation (14): a degree- Bernstein sum in equals a degree- Bernstein sum whose coefficients are hypergeometric averages of the original ones.
Preamble
import Definitions.Def_GameSetMatchInternal
Formal statement
namespace GameSetMatch
/-- Bernstein degree elevation with hypergeometric weights. -/
theorem bernstein_elevate (M n : ℕ) (hM : 1 ≤ M) (r : ℝ) (f : ℕ → ℝ) :
∑ l ∈ Finset.range (n + 1), (n.choose l : ℝ) * r ^ l * (1 - r) ^ (n - l) * f l
= ∑ i ∈ Finset.range (M * n + 1),
((M * n).choose i : ℝ) * r ^ i * (1 - r) ^ (M * n - i) *
∑ l ∈ Finset.range (n + 1), hypergeomWeight M n i l * f l := by
sorry
end GameSetMatchSource
four_part_nested_best_of_proof.md (private notes, 3 Sep 2026)
Human review
Confirmed by the mission captain (proposal self-audit).