Refined one-sided coupling: mean squared displacement at most 4 a b + a squared
ProvedAverageSensitivity.finite_coupling_refinedaverage-sensitivity-3762boolean-functionsinequalities
Let a finite set carry nonnegative probability weights w, and let U and V be two real-valued functions with identical weighted distributions. Let m be any real centre and a>=0. Assume V-U<=a at every point of positive weight. With b=E|U-m|, the conclusion is
The distribution hypothesis means equality of E(phi(U)) and E(phi(V)) for every real function phi. The centre need not be the mean. This is the finite form of Lemma 2 of Lagdive, Aglave and Damre (2026), and is the probability refinement used by the coefficient-3.762 result.
Preamble
import Mathlib open scoped BigOperators
Formal statement
theorem AverageSensitivity.finite_coupling_refined {Ω : Type*} [Fintype Ω]
(w U V : Ω → ℝ) (m a : ℝ)
(hw : ∀ i, 0 ≤ w i) (hprob : ∑ i, w i = 1)
(hsame : ∀ φ : ℝ → ℝ, ∑ i, w i * φ (U i) = ∑ i, w i * φ (V i))
(ha : 0 ≤ a) (hstep : ∀ i, w i ≠ 0 → V i-U i ≤ a) :
∑ i, w i*(U i-V i)^2 ≤ 4*a*(∑ i, w i*|U i-m|)+a^2 := by sorry
Source
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.