Gotsman--Linial: influence of polynomial threshold functions

OpenAI, Average Sensitivity of Polynomial Threshold Functions (25 September 2026): https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Average-Sensitivity-of-Polynomial-Threshold-Functions-September-25-2026

The imported proof establishes the bound 8 * d * sqrt n on average sensitivity. The bridge identifies average sensitivity with complexitylib's Fourier total influence. A checked multilinearization removes the source statement's multilinearity hypothesis, so the public bound accepts any real polynomial. The sign convention is sign(0) = 1, with no nonvanishing hypothesis.

The noise and Fourier-tail estimates below combine this bound with the library's existing Fourier API. They are elementary consequences, not claims of new research results or of the sharper dimension-free noise bound in the source paper.

theorem Complexity.BooleanAnalysis.signMultilinearize_totalDegree_le {n : ℕ} (p : MvPolynomial (Fin n) ℝ) : (signMultilinearize p).totalDegree ≤ p.totalDegree

Sign-cube multilinearization does not increase total degree.

theorem Complexity.BooleanAnalysis.signMultilinearize_eval {n : ℕ} (p : MvPolynomial (Fin n) ℝ) (x : Fin n → ℝ) (hx : ∀ (i : Fin n), x i ^ 2 = 1) : (MvPolynomial.eval x) (signMultilinearize p) = (MvPolynomial.eval x) p

Reducing exponents modulo two preserves evaluation whenever all coordinates square to one.

theorem Complexity.BooleanAnalysis.polynomialThreshold_signMultilinearize {n : ℕ} (p : MvPolynomial (Fin n) ℝ) : polynomialThreshold (signMultilinearize p) = polynomialThreshold p

Multilinearization preserves the threshold, including its values at polynomial zeros.

theorem Complexity.BooleanAnalysis.isBooleanValued_polynomialThreshold {n : ℕ} (p : MvPolynomial (Fin n) ℝ) : IsBooleanValued (polynomialThreshold p)

A polynomial threshold always takes values in {-1, 1}.

theorem Complexity.BooleanAnalysis.totalInfluence_polynomialThreshold_le {n d : ℕ} (p : MvPolynomial (Fin n) ℝ) (hd : p.totalDegree ≤ d) : totalInfluence (polynomialThreshold p) ≤ 8 * ↑d * √↑n

Gotsman--Linial bound. Every degree-d real polynomial threshold has total influence at most 8 * d * sqrt n. Dimensions and degrees may be zero.

theorem Complexity.BooleanAnalysis.IsPolynomialThreshold.totalInfluence_le {n d : ℕ} {f : BooleanFunction n} (hf : IsPolynomialThreshold f d) : totalInfluence f ≤ 8 * ↑d * √↑n

The influence bound in terms of the represented function and its threshold degree.

theorem Complexity.BooleanAnalysis.IsPolynomialThreshold.noiseSensitivity_le {n d : ℕ} {f : BooleanFunction n} (hf : IsPolynomialThreshold f d) {ρ : ℝ} (hρ0 : 0 ≤ ρ) (hρ1 : ρ ≤ 1) : noiseSensitivity ρ f ≤ 4 * (1 - ρ) * ↑d * √↑n

Degree bounds on a threshold imply the corresponding spectral noise bound. Here ρ is the correlation parameter; the bit-flip rate is (1 - ρ) / 2.

theorem Complexity.BooleanAnalysis.IsPolynomialThreshold.fourierWeightAbove_le {n d : ℕ} {f : BooleanFunction n} (hf : IsPolynomialThreshold f d) (m : ℕ) : fourierWeightAbove f m ≤ 8 * ↑d * √↑n / (↑m + 1)

Above Fourier degree m, a degree-d polynomial threshold has total Fourier weight at most 8 * d * sqrt n / (m + 1).