Gotsman--Linial: WalshDimensions

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

Dimensions of the Walsh degree filtration, derived from the linear independence of the concrete characters.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.card_finset_card_le (n k : ℕ) : Fintype.card { S : Finset (Fin n) // S.card ≤ k } = ∑ j ∈ Finset.range (k + 1), n.choose j

Count low-degree character indices by partitioning them according to cardinality.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fourierSpace_finrank (n k : ℕ) : Module.finrank ℂ ↥(fourierSpace n k) = ∑ j ∈ Finset.range (k + 1), n.choose j

The dimension of the degree-k Fourier subspace is the number of indices of cardinality at most k. This formula remains valid beyond the saturated stage.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fourierSpace_finrank_add (n k : ℕ) : Module.finrank ℂ ↥(fourierSpace n k) + n.choose (k + 1) = Module.finrank ℂ ↥(fourierSpace n (k + 1))

Each new degree contributes exactly the next binomial multiplicity.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fourierSpace_finrank_sub (n k : ℕ) : Module.finrank ℂ ↥(fourierSpace n (k + 1)) - Module.finrank ℂ ↥(fourierSpace n k) = n.choose (k + 1)

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fourierSpace_zero_finrank (n : ℕ) : Module.finrank ℂ ↥(fourierSpace n 0) = 1

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fourierSpace_finrank_of_le {n k : ℕ} (hnk : n ≤ k) : Module.finrank ℂ ↥(fourierSpace n k) = 2 ^ n

At or above degree n, the Fourier space has the full cube dimension.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.map_fourierSpace_finrank {E : Type u_1} [AddCommGroup E] [Module ℂ E] (n k : ℕ) (D : (Cube n → ℂ) ≃ₗ[ℂ] E) : Module.finrank ℂ ↥(Submodule.map (↑D) (fourierSpace n k)) = ∑ j ∈ Finset.range (k + 1), n.choose j

Arbitrary invertible linear changes of coordinates preserve every Fourier dimension.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fourierEuclideanSpace_finrank (n k : ℕ) : Module.finrank ℂ ↥(fourierEuclideanSpace n k) = ∑ j ∈ Finset.range (k + 1), n.choose j

Passing to the counting Euclidean Hilbert space changes no dimensions.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fourierFlag_finrank (n k : ℕ) : Module.finrank ℂ ↥(fourierFlag n k) = ∑ j ∈ Finset.range k, n.choose j

With the bottom stage inserted, stage k contains exactly degrees below k.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fourierFlag_finrank_add (n k : ℕ) : Module.finrank ℂ ↥(fourierFlag n k) + n.choose k = Module.finrank ℂ ↥(fourierFlag n (k + 1))

The degree-k layer has the prescribed binomial dimension increment.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fourierFlag_finrank_sub (n k : ℕ) : Module.finrank ℂ ↥(fourierFlag n (k + 1)) - Module.finrank ℂ ↥(fourierFlag n k) = n.choose k

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.map_fourierFlag_finrank (n k : ℕ) (D : EuclideanSpace ℂ (Cube n) ≃ₗ[ℂ] EuclideanSpace ℂ (Cube n)) : Module.finrank ℂ ↥(Submodule.map (↑D) (fourierFlag n k)) = ∑ j ∈ Finset.range k, n.choose j

Any invertible weight preserves the dimensions of all stages of the Euclidean flag.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.map_fourierFlag_finrank_add (n k : ℕ) (D : EuclideanSpace ℂ (Cube n) ≃ₗ[ℂ] EuclideanSpace ℂ (Cube n)) : Module.finrank ℂ ↥(Submodule.map (↑D) (fourierFlag n k)) + n.choose k = Module.finrank ℂ ↥(Submodule.map (↑D) (fourierFlag n (k + 1)))

In particular, an invertible weight preserves each binomial dimension increment.