Gotsman--Linial: Walsh

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

Walsh characters of the Boolean cube

The characters are the real sign monomials, regarded as complex-valued functions. Counting orthogonality proves linear independence; the cardinality comparison then gives a basis. The degree filtration and its dimensions are constructed from this concrete basis.

def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.walshChar {n : ℕ} (S : Finset (Fin n)) (x : Cube n) : ℂ

The complex-valued Walsh character associated to a subset of coordinates.

Equations

• Complexity.BooleanAnalysis.PolynomialThreshold.Internal.walshChar S x = ∏ i ∈ S, ↑(Complexity.BooleanAnalysis.PolynomialThreshold.Internal.cubeCoord x i)

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.walshChar_empty {n : ℕ} (x : Cube n) : walshChar ∅ x = 1

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.walshChar_singleton {n : ℕ} (i : Fin n) (x : Cube n) : walshChar {i} x = ↑(cubeCoord x i)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.walshChar_eq_prod_univ {n : ℕ} (S : Finset (Fin n)) (x : Cube n) : walshChar S x = ∏ i : Fin n, if i ∈ S then ↑(cubeCoord x i) else 1

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.star_walshChar {n : ℕ} (S : Finset (Fin n)) (x : Cube n) : star (walshChar S x) = walshChar S x

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.walshChar_mul {n : ℕ} (S T : Finset (Fin n)) (x : Cube n) : walshChar S x * walshChar T x = walshChar (symmDiff S T) x

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.walshChar_mul_self {n : ℕ} (S : Finset (Fin n)) (x : Cube n) : walshChar S x * walshChar S x = 1

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.walshChar_univ_mul {n : ℕ} (S : Finset (Fin n)) (x : Cube n) : walshChar Finset.univ x * walshChar S x = walshChar (Finset.univ \ S) x

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sum_walshChar {n : ℕ} (S : Finset (Fin n)) : ∑ x : Cube n, walshChar S x = if S = ∅ then 2 ^ n else 0

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.walshChar_orthogonality {n : ℕ} (S T : Finset (Fin n)) : ∑ x : Cube n, star (walshChar S x) * walshChar T x = if S = T then 2 ^ n else 0

Orthogonality for the unnormalized counting inner product.

def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.walshCoefficientLinear {n : ℕ} (S : Finset (Fin n)) : (Cube n → ℂ) →ₗ[ℂ] ℂ

Unnormalized Fourier coefficient as a linear functional.

Equations

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

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.walshCoefficientLinear_char {n : ℕ} (S T : Finset (Fin n)) : (walshCoefficientLinear S) (walshChar T) = if S = T then 2 ^ n else 0

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.walshChar_linearIndependent (n : ℕ) : LinearIndependent ℂ walshChar

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.walsh_index_card (n : ℕ) : Fintype.card (Finset (Fin n)) = Module.finrank ℂ (Cube n → ℂ)

noncomputable def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.walshBasis (n : ℕ) : Module.Basis (Finset (Fin n)) ℂ (Cube n → ℂ)

The concrete Walsh basis, indexed by coordinate subsets.

Equations

• Complexity.BooleanAnalysis.PolynomialThreshold.Internal.walshBasis n = basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.walshBasis_apply {n : ℕ} (S : Finset (Fin n)) : (walshBasis n) S = walshChar S

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

Functions of Fourier degree at most k.

Equations

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

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fourierSpace_mono (n : ℕ) : Monotone (fourierSpace n)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fourierSpace_eq_top {n k : ℕ} (hk : n ≤ k) : fourierSpace n k = ⊤

def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fourierEuclideanSpace (n k : ℕ) : Submodule ℂ (EuclideanSpace ℂ (Cube n))

Fourier degree filtration in the Hilbert space with counting inner product.

Equations

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

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.mem_fourierEuclideanSpace {n k : ℕ} (f : EuclideanSpace ℂ (Cube n)) : f ∈ fourierEuclideanSpace n k ↔ (fun (x : Cube n) => f.ofLp x) ∈ fourierSpace n k

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fourierEuclideanSpace_mono (n : ℕ) : Monotone (fourierEuclideanSpace n)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fourierEuclideanSpace_eq_top {n k : ℕ} (hk : n ≤ k) : fourierEuclideanSpace n k = ⊤

def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fourierFlag (n a✝ : ℕ) : Submodule ℂ (EuclideanSpace ℂ (Cube n))

Shift the degree filtration so that its zeroth member is bottom.

Equations

• Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fourierFlag n 0 = ⊥
• Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fourierFlag n k.succ = Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fourierEuclideanSpace n k

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fourierFlag_zero (n : ℕ) : fourierFlag n 0 = ⊥

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fourierFlag_succ (n k : ℕ) : fourierFlag n (k + 1) = fourierEuclideanSpace n k

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fourierFlag_mono (n : ℕ) : Monotone (fourierFlag n)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fourierFlag_top (n : ℕ) : fourierFlag n (n + 1) = ⊤