Gotsman--Linial: PolynomialDegree

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

Polynomial degree and the Walsh filtration

The polynomial lemmas concern real multilinear MvPolynomials. Restriction to the cube is justified by an explicit monomial expansion rather than assumed as an alternate polynomial representation.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.IsMultilinear.add_C {n : ℕ} {p : MvPolynomial (Fin n) ℝ} (hp : IsMultilinear p) (c : ℝ) : IsMultilinear (p + MvPolynomial.C c)

Adding a constant preserves the multilinearity condition.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.totalDegree_add_C_le {n d : ℕ} {p : MvPolynomial (Fin n) ℝ} (hd : p.totalDegree ≤ d) (c : ℝ) : (p + MvPolynomial.C c).totalDegree ≤ d

Adding a constant cannot violate an existing total-degree upper bound.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.IsMultilinear.exponent_eq_one {n : ℕ} {p : MvPolynomial (Fin n) ℝ} (hp : IsMultilinear p) {m : Fin n →₀ ℕ} (hm : m ∈ p.support) {i : Fin n} (hi : i ∈ m.support) : m i = 1

Every exponent occurring in a supported multilinear monomial is one.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.monomial_support_card_le_totalDegree {n : ℕ} {p : MvPolynomial (Fin n) ℝ} {m : Fin n →₀ ℕ} (hm : m ∈ p.support) : m.support.card ≤ p.totalDegree

A supported monomial has no more variables than the polynomial's total degree. This estimate does not require multilinearity.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.polynomialValue_eq_multilinear_expansion {n : ℕ} {p : MvPolynomial (Fin n) ℝ} (hp : IsMultilinear p) (x : Cube n) : polynomialValue p x = ∑ m ∈ p.support, p.coeff m * ∏ i ∈ m.support, cubeCoord x i

Faithful evaluation of a multilinear polynomial as products over the supports of its monomials.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.polynomialValue_walsh_expansion {n : ℕ} {p : MvPolynomial (Fin n) ℝ} (hp : IsMultilinear p) (x : Cube n) : ↑(polynomialValue p x) = ∑ m ∈ p.support, ↑(p.coeff m) * walshChar m.support x

The same faithful expansion, with values regarded as complex numbers.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.walshChar_mem_fourierSpace {n d : ℕ} {S : Finset (Fin n)} (hS : S.card ≤ d) : walshChar S ∈ fourierSpace n d

A character of degree at most d belongs to the corresponding filtration.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.polynomialValue_mem_fourierSpace {n d : ℕ} {p : MvPolynomial (Fin n) ℝ} (hp : IsMultilinear p) (hd : p.totalDegree ≤ d) : (fun (x : Cube n) => ↑(polynomialValue p x)) ∈ fourierSpace n d

The exact polynomial bridge into the complex Walsh filtration.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fourierSpace_star {n d : ℕ} {a : Cube n → ℂ} (ha : a ∈ fourierSpace n d) : star a ∈ fourierSpace n d

Complex conjugation preserves Fourier degree, since each character is real.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fourierSpace_mul {n r s : ℕ} {a b : Cube n → ℂ} (ha : a ∈ fourierSpace n r) (hb : b ∈ fourierSpace n s) : a * b ∈ fourierSpace n (r + s)

The filtration is multiplicative. The symmetric difference of two index sets has cardinality at most the sum of their cardinalities.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fourierSpace_conj_mul {n r s : ℕ} {a b : Cube n → ℂ} (ha : a ∈ fourierSpace n r) (hb : b ∈ fourierSpace n s) : (fun (x : Cube n) => star (b x) * a x) ∈ fourierSpace n (r + s)

The precise multiplication-conjugation rule used in the weighted pairing.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.cubeCoord_mul_mem_fourierSpace {n r : ℕ} {a : Cube n → ℂ} (ha : a ∈ fourierSpace n r) (i : Fin n) : (fun (x : Cube n) => ↑(cubeCoord x i) * a x) ∈ fourierSpace n (r + 1)

Multiplication by one cube coordinate raises the degree by at most one.

def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fourierSpaceFrom (n k : ℕ) : Submodule ℂ (Cube n → ℂ)

Functions whose Walsh support starts in degree k.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.walshChar_mem_fourierSpaceFrom {n d : ℕ} {S : Finset (Fin n)} (hS : d ≤ S.card) : walshChar S ∈ fourierSpaceFrom n d

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.parity_mul_mem_fourierSpaceFrom {n d : ℕ} {a : Cube n → ℂ} (ha : a ∈ fourierSpace n d) : (fun (x : Cube n) => walshChar Finset.univ x * a x) ∈ fourierSpaceFrom n (n - d)

Full parity complements character index sets, taking low degree d to Fourier support in degrees at least n - d.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sum_mul_eq_zero_of_fourier_separated {n r s : ℕ} {a b : Cube n → ℂ} (ha : a ∈ fourierSpace n r) (hb : b ∈ fourierSpaceFrom n s) (hrs : r < s) : ∑ x : Cube n, a x * b x = 0

Low and high Fourier support with a strict gap have zero counting pairing. There is no conjugation in this formulation because Walsh characters are real; it applies directly to the product appearing in the weighted proof.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.parity_polynomialValue_mem_fourierSpaceFrom {n d : ℕ} {p : MvPolynomial (Fin n) ℝ} (hp : IsMultilinear p) (hd : p.totalDegree ≤ d) : (fun (x : Cube n) => walshChar Finset.univ x * ↑(polynomialValue p x)) ∈ fourierSpaceFrom n (n - d)

The polynomial has high Fourier support after multiplication by full parity, with no alternate polynomial-class assumption.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.parity_polynomialValue_low_coefficient_eq_zero {n d : ℕ} {p : MvPolynomial (Fin n) ℝ} (hp : IsMultilinear p) (hd : p.totalDegree ≤ d) {S : Finset (Fin n)} (hS : S.card < n - d) : ((walshCoefficientLinear S) fun (x : Cube n) => walshChar Finset.univ x * ↑(polynomialValue p x)) = 0

Every Fourier coefficient below n - d of the parity-transformed polynomial vanishes.