Gotsman--Linial: WeightedGrading

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

The actual weighted orthogonal grading of the cube

The construction first orthogonalizes an arbitrary finite flag of subspaces. It then transports the concrete Walsh flag by the invertible square-root weight and takes the orthogonal projections in the counting Hilbert space. The resulting matrices are proved to form an orthogonal decomposition of the identity with the prescribed binomial multiplicities.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.instCompleteSpace_complexitylib_1 {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] : CompleteSpace E

def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flagLayer {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : ℕ → Submodule 𝕜 E) (k : ℕ) : Submodule 𝕜 E

The new orthogonal layer appearing between two consecutive stages of a flag.

Equations

• Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flagLayer K k = K (k + 1) ⊓ (K k)ᗮ

noncomputable def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flagProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (K : ℕ → Submodule 𝕜 E) (k : ℕ) : E →L[𝕜] E

The actual orthogonal projection onto a layer of a finite-dimensional flag.

Equations

• Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flagProjection K k = (Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flagLayer K k).starProjection

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flagLayer_le_next {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : ℕ → Submodule 𝕜 E) (k : ℕ) : flagLayer K k ≤ K (k + 1)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flagLayer_le_prev_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : ℕ → Submodule 𝕜 E) (k : ℕ) : flagLayer K k ≤ (K k)ᗮ

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flagLayer_sup_prev {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (K : ℕ → Submodule 𝕜 E) (hK : Monotone K) (k : ℕ) : K k ⊔ flagLayer K k = K (k + 1)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flagLayer_finrank_add {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (K : ℕ → Submodule 𝕜 E) (hK : Monotone K) (k : ℕ) : Module.finrank 𝕜 ↥(K k) + Module.finrank 𝕜 ↥(flagLayer K k) = Module.finrank 𝕜 ↥(K (k + 1))

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flagLayer_finrank {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (K : ℕ → Submodule 𝕜 E) (hK : Monotone K) (k : ℕ) : Module.finrank 𝕜 ↥(flagLayer K k) = Module.finrank 𝕜 ↥(K (k + 1)) - Module.finrank 𝕜 ↥(K k)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flagLayer_isOrtho_of_lt {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : ℕ → Submodule 𝕜 E) (hK : Monotone K) {r s : ℕ} (hrs : r < s) : flagLayer K r ⟂ flagLayer K s

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flagLayer_isOrtho {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : ℕ → Submodule 𝕜 E) (hK : Monotone K) {r s : ℕ} (hrs : r ≠ s) : flagLayer K r ⟂ flagLayer K s

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flagLayer_iSup_eq_top {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (K : ℕ → Submodule 𝕜 E) (hK : Monotone K) (hzero : K 0 = ⊥) (n : ℕ) (htop : K (n + 1) = ⊤) : ⨆ (k : Fin (n + 1)), flagLayer K ↑k = ⊤

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flagLayer_orthogonalFamily {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : ℕ → Submodule 𝕜 E) (hK : Monotone K) (n : ℕ) : OrthogonalFamily 𝕜 (fun (k : Fin (n + 1)) => ↥(flagLayer K ↑k)) fun (k : Fin (n + 1)) => (flagLayer K ↑k).subtypeₗᵢ

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flagProjection_isSelfAdjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (K : ℕ → Submodule 𝕜 E) (k : ℕ) : IsSelfAdjoint (flagProjection K k)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flagProjection_idempotent {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (K : ℕ → Submodule 𝕜 E) (k : ℕ) : flagProjection K k * flagProjection K k = flagProjection K k

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flagProjection_mul_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (K : ℕ → Submodule 𝕜 E) (hK : Monotone K) {r s : ℕ} (hrs : r ≠ s) : flagProjection K r * flagProjection K s = 0

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sum_flagProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (K : ℕ → Submodule 𝕜 E) (hK : Monotone K) (hzero : K 0 = ⊥) (n : ℕ) (htop : K (n + 1) = ⊤) : ∑ k : Fin (n + 1), flagProjection K ↑k = 1

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.range_flagProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (K : ℕ → Submodule 𝕜 E) (k : ℕ) : (↑(flagProjection K k)).range = flagLayer K k

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flagProjection_apply_mem_next {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (K : ℕ → Submodule 𝕜 E) (k : ℕ) (x : E) : (flagProjection K k) x ∈ K (k + 1)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flagProjection_apply_eq_zero_of_mem_prev {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (K : ℕ → Submodule 𝕜 E) (k : ℕ) {x : E} (hx : x ∈ K k) : (flagProjection K k) x = 0

noncomputable def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.coordinateMulEquiv {Ω : Type u_1} (a : Ω → ℂ) (ha : ∀ (x : Ω), a x ≠ 0) : (Ω → ℂ) ≃ₗ[ℂ] Ω → ℂ

Multiplication by pointwise nonzero coefficients is a linear equivalence.

Equations

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

noncomputable def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sqrtWeightEquiv {Ω : Type u_1} (w : Ω → ℝ) (hw : ∀ (x : Ω), 0 < w x) : EuclideanSpace ℂ Ω ≃ₗ[ℂ] EuclideanSpace ℂ Ω

Multiplication by the square root of a strictly positive weight, in the counting Euclidean Hilbert space.

Equations

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

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sqrtWeightEquiv_apply {Ω : Type u_1} (w : Ω → ℝ) (hw : ∀ (x : Ω), 0 < w x) (f : EuclideanSpace ℂ Ω) (x : Ω) : ((sqrtWeightEquiv w hw) f).ofLp x = ↑√(w x) * f.ofLp x

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sqrtWeightEquiv_symm_apply {Ω : Type u_1} (w : Ω → ℝ) (hw : ∀ (x : Ω), 0 < w x) (f : EuclideanSpace ℂ Ω) (x : Ω) : ((sqrtWeightEquiv w hw).symm f).ofLp x = (↑√(w x))⁻¹ * f.ofLp x

def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.transportFlag {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (D : E ≃ₗ[𝕜] E) (F : ℕ → Submodule 𝕜 E) (k : ℕ) : Submodule 𝕜 E

Transport a degree flag through an invertible linear weight operator.

Equations

• Complexity.BooleanAnalysis.PolynomialThreshold.Internal.transportFlag D F k = Submodule.map (↑D) (F k)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.transportFlag_monotone {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (D : E ≃ₗ[𝕜] E) (F : ℕ → Submodule 𝕜 E) (hF : Monotone F) : Monotone (transportFlag D F)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.transportFlag_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (D : E ≃ₗ[𝕜] E) (F : ℕ → Submodule 𝕜 E) (hF : F 0 = ⊥) : transportFlag D F 0 = ⊥

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.transportFlag_top {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (D : E ≃ₗ[𝕜] E) (F : ℕ → Submodule 𝕜 E) (k : ℕ) (hF : F k = ⊤) : transportFlag D F k = ⊤

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.transportFlag_finrank {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (D : E ≃ₗ[𝕜] E) (F : ℕ → Submodule 𝕜 E) (k : ℕ) : Module.finrank 𝕜 ↥(transportFlag D F k) = Module.finrank 𝕜 ↥(F k)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.transportFlag_layer_finrank {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (D : E ≃ₗ[𝕜] E) (F : ℕ → Submodule 𝕜 E) (hF : Monotone F) (k d : ℕ) (hd : Module.finrank 𝕜 ↥(F k) + d = Module.finrank 𝕜 ↥(F (k + 1))) : Module.finrank 𝕜 ↥(flagLayer (transportFlag D F) k) = d

The weighted construction preserves every prescribed dimension increment.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.instCompleteSpace_complexitylib_2 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] : CompleteSpace E

noncomputable def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flagProjectionMatrix {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] [Fintype ι] [DecidableEq ι] (b : OrthonormalBasis ι ℂ E) (K : ℕ → Submodule ℂ E) (k : ℕ) : Matrix ι ι ℂ

Matrix of an actual flag-layer projection in an orthonormal basis.

Equations

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

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flagProjectionMatrix_family {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] [Fintype ι] [DecidableEq ι] (b : OrthonormalBasis ι ℂ E) (K : ℕ → Submodule ℂ E) (hK : Monotone K) (hzero : K 0 = ⊥) (n : ℕ) (htop : K (n + 1) = ⊤) : OrthogonalProjectionFamily fun (k : Fin (n + 1)) => flagProjectionMatrix b K ↑k

The matrix projection-family laws follow from the constructed Hilbert-space projections, without any additional grading hypothesis.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.trace_flagProjectionMatrix {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] [Fintype ι] [DecidableEq ι] (b : OrthonormalBasis ι ℂ E) (K : ℕ → Submodule ℂ E) (k : ℕ) : (flagProjectionMatrix b K k).trace = ↑(Module.finrank ℂ ↥(flagLayer K k))

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.re_trace_flagProjectionMatrix {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] [Fintype ι] [DecidableEq ι] (b : OrthonormalBasis ι ℂ E) (K : ℕ → Submodule ℂ E) (k : ℕ) : (flagProjectionMatrix b K k).trace.re = ↑(Module.finrank ℂ ↥(flagLayer K k))

noncomputable def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.weightedFourierSpace {n : ℕ} (w : Cube n → ℝ) (hw : ∀ (x : Cube n), 0 < w x) (k : ℕ) : Submodule ℂ (EuclideanSpace ℂ (Cube n))

The weighted degree-k subspace of the counting Hilbert space.

Equations

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

noncomputable def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.weightedFourierFlag {n : ℕ} (w : Cube n → ℝ) (hw : ∀ (x : Cube n), 0 < w x) : ℕ → Submodule ℂ (EuclideanSpace ℂ (Cube n))

The weighted Fourier flag, shifted by one so that stage zero is bottom.

Equations

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

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.weightedFourierFlag_zero {n : ℕ} (w : Cube n → ℝ) (hw : ∀ (x : Cube n), 0 < w x) : weightedFourierFlag w hw 0 = ⊥

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.weightedFourierFlag_succ {n : ℕ} (w : Cube n → ℝ) (hw : ∀ (x : Cube n), 0 < w x) (k : ℕ) : weightedFourierFlag w hw (k + 1) = weightedFourierSpace w hw k

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.weightedFourierFlag_mono {n : ℕ} (w : Cube n → ℝ) (hw : ∀ (x : Cube n), 0 < w x) : Monotone (weightedFourierFlag w hw)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.weightedFourierFlag_top {n : ℕ} (w : Cube n → ℝ) (hw : ∀ (x : Cube n), 0 < w x) : weightedFourierFlag w hw (n + 1) = ⊤

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.weightedFourierFlag_layer_finrank {n : ℕ} (w : Cube n → ℝ) (hw : ∀ (x : Cube n), 0 < w x) (k : ℕ) : Module.finrank ℂ ↥(flagLayer (weightedFourierFlag w hw) k) = n.choose k

Weighting preserves the exact binomial dimensions of the orthogonal layers.

noncomputable def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.weightedProjection {n : ℕ} (w : Cube n → ℝ) (hw : ∀ (x : Cube n), 0 < w x) (k : Fin (n + 1)) : EuclideanSpace ℂ (Cube n) →L[ℂ] EuclideanSpace ℂ (Cube n)

Actual orthogonal projection onto weighted Fourier layer k.

Equations

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

noncomputable def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.weightedProjectionMatrix {n : ℕ} (w : Cube n → ℝ) (hw : ∀ (x : Cube n), 0 < w x) (k : Fin (n + 1)) : Matrix (Cube n) (Cube n) ℂ

The projection represented in the point-mass orthonormal basis.

Equations

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

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.weightedProjection_apply_mem {n : ℕ} (w : Cube n → ℝ) (hw : ∀ (x : Cube n), 0 < w x) (k : Fin (n + 1)) (f : EuclideanSpace ℂ (Cube n)) : (weightedProjection w hw k) f ∈ weightedFourierSpace w hw ↑k

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.weightedProjection_annihilate_prev {n : ℕ} (w : Cube n → ℝ) (hw : ∀ (x : Cube n), 0 < w x) (k : Fin (n + 1)) {f : EuclideanSpace ℂ (Cube n)} (hf : f ∈ weightedFourierFlag w hw ↑k) : (weightedProjection w hw k) f = 0

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.weightedProjectionMatrix_family {n : ℕ} (w : Cube n → ℝ) (hw : ∀ (x : Cube n), 0 < w x) : OrthogonalProjectionFamily (weightedProjectionMatrix w hw)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.weightedProjectionMatrix_trace {n : ℕ} (w : Cube n → ℝ) (hw : ∀ (x : Cube n), 0 < w x) (k : Fin (n + 1)) : (weightedProjectionMatrix w hw k).trace = ↑(n.choose ↑k)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.weightedProjectionMatrix_trace_re {n : ℕ} (w : Cube n → ℝ) (hw : ∀ (x : Cube n), 0 < w x) (k : Fin (n + 1)) : (weightedProjectionMatrix w hw k).trace.re = ↑(n.choose ↑k)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.weightedProjectionMatrix_hsNormSq {n : ℕ} (w : Cube n → ℝ) (hw : ∀ (x : Cube n), 0 < w x) (k : Fin (n + 1)) : hsNormSq (weightedProjectionMatrix w hw k) = ↑(n.choose ↑k)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sqrtWeightEquiv_commute_signMultiplier {n : ℕ} (w : Cube n → ℝ) (hw : ∀ (x : Cube n), 0 < w x) (h : Cube n → ℝ) (f : EuclideanSpace ℂ (Cube n)) : (signMultiplier h) ((sqrtWeightEquiv w hw) f) = (sqrtWeightEquiv w hw) ((signMultiplier h) f)

Every real diagonal multiplier commutes with the positive square-root weight.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sqrtWeightEquiv_commute_coordinateMultiplier {n : ℕ} (w : Cube n → ℝ) (hw : ∀ (x : Cube n), 0 < w x) (i : Fin n) (f : EuclideanSpace ℂ (Cube n)) : (coordinateMultiplier i) ((sqrtWeightEquiv w hw) f) = (sqrtWeightEquiv w hw) ((coordinateMultiplier i) f)