Gotsman--Linial: FiniteCoupling

Adapted from OpenAI's formalization of Average Sensitivity of Polynomial Threshold Functions (25 September 2026), at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/GotsmanLinial/FiniteCoupling.lean

The original Boolean-cube representation is used internally in this proof development; Complexitylib.BooleanAnalysis.PolynomialThreshold transports the result to the library's Fourier and influence API. Changes here adapt module visibility, namespace names, formatting, and redundant simp attributes to complexitylib.

A finite one-sided coupling estimate

This is a finite weighted probabilistic estimate. Equal marginals are expressed as equality of the weighted expectations of every real function. The increment bound is required only on the support of the nonnegative probability weights.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.weighted_abs_le_of_second_moment {Ω : Type u_1} [Fintype Ω] (w f : Ω → ℝ) (σ : ℝ) (hw : ∀ (i : Ω), 0 ≤ w i) (hprob : ∑ i : Ω, w i = 1) (hσ : 0 ≤ σ) (hsecond : ∑ i : Ω, w i * f i ^ 2 ≤ σ ^ 2) : ∑ i : Ω, w i * |f i| ≤ σ

Weighted Cauchy--Schwarz bounds the first absolute moment by a bound on the second moment. Zero weights are allowed.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.weighted_abs_eq_twice_positive_part {Ω : Type u_1} [Fintype Ω] (w z : Ω → ℝ) (hzero : ∑ i : Ω, w i * z i = 0) : ∑ i : Ω, w i * |z i| = 2 * ∑ i : Ω, w i * max (z i) 0

A weighted mean-zero variable has absolute first moment twice the first moment of its positive part. This identity does not need positivity of the weights.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.finite_one_sided_coupling_bound {Ω : Type u_1} [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)) (hσ : 0 ≤ σ) (ha : 0 ≤ a) (hvariance : ∑ i : Ω, w i * (U i - m) ^ 2 = σ ^ 2) (hstep : ∀ (i : Ω), w i ≠ 0 → V i - U i ≤ a) : ∑ i : Ω, w i * (U i - V i) ^ 2 ≤ 8 * a * σ

The finite one-sided coupling lemma: identical marginals and an upper bound a on V - U bound the mean square displacement by 8 * a * σ.

The center m may be arbitrary. Taking it to be the common mean recovers the variance bound with variance σ²; only the displayed second moment is used.