Documentation

Complexitylib.BooleanAnalysis.PolynomialThreshold.Internal.ScalarIncrements

Gotsman--Linial: ScalarIncrements #

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/ScalarIncrements.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.

Scalar inequalities for the one-sided coupling estimate #

The increasing function couplingPotential m t = (t-m)|t-m|/2 controls squared distances from below and has a trapezoidal increment bound from above. All arguments here are algebraic, by splitting according to the positions of the endpoints relative to the center m.

source
noncomputable def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.couplingPotential (m t : ℝ) :
ℝ

The scalar potential used in the one-sided coupling argument.

Equations
Instances For
    source
    @[simp]
    theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.couplingPotential_self (m : ℝ) :
    couplingPotential m m = 0
    source
    theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.couplingPotential_increment_bounds (m : ℝ) {u v : ℝ} (huv : u ≤ v) :
    (v - u) ^ 2 / 4 ≤ couplingPotential m v - couplingPotential m u ∧ couplingPotential m v - couplingPotential m u ≤ (v - u) / 2 * (|u - m| + |v - m|)

    Both increment inequalities hold even when the endpoints coincide.

    source
    theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.couplingPotential_increment_lower (m : ℝ) {u v : ℝ} (huv : u ≤ v) :
    (v - u) ^ 2 / 4 ≤ couplingPotential m v - couplingPotential m u
    source
    theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.couplingPotential_increment_upper (m : ℝ) {u v : ℝ} (huv : u ≤ v) :
    couplingPotential m v - couplingPotential m u ≤ (v - u) / 2 * (|u - m| + |v - m|)
    source
    theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.monotone_couplingPotential (m : ℝ) :
    Monotone (couplingPotential m)
    source
    theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.strictMono_couplingPotential (m : ℝ) :
    StrictMono (couplingPotential m)
    source
    @[simp]
    theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.couplingPotential_le_iff (m u v : ℝ) :
    couplingPotential m u ≤ couplingPotential m v ↔ u ≤ v
    source
    @[simp]
    theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.couplingPotential_lt_iff (m u v : ℝ) :
    couplingPotential m u < couplingPotential m v ↔ u < v
    source
    @[simp]
    theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.couplingPotential_eq_iff (m u v : ℝ) :
    couplingPotential m u = couplingPotential m v ↔ u = v
    source
    theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.couplingPotential_sub_nonneg_iff (m u v : ℝ) :
    0 ≤ couplingPotential m v - couplingPotential m u ↔ u ≤ v
    source
    theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.couplingPotential_sub_pos_iff (m u v : ℝ) :
    0 < couplingPotential m v - couplingPotential m u ↔ u < v
    source
    theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.abs_couplingPotential_sub_of_le (m : ℝ) {u v : ℝ} (huv : u ≤ v) :
    |couplingPotential m v - couplingPotential m u| = couplingPotential m v - couplingPotential m u
    source
    theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sq_sub_le_four_mul_abs_potential_sub (m u v : ℝ) :
    (u - v) ^ 2 ≤ 4 * |couplingPotential m u - couplingPotential m v|

    The pointwise lower bound in the coupling argument, without ordering the two real variables.

    source
    theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.max_couplingPotential_increment_le (m a u v : ℝ) (ha : 0 ≤ a) (hstep : v - u ≤ a) :
    max (couplingPotential m v - couplingPotential m u) 0 ≤ a / 2 * (|u - m| + |v - m|)

    An upper bound for the positive part of a potential increment under a one-sided bound on the original increment.