Documentation

Complexitylib.BooleanAnalysis.PolynomialThreshold.Internal.ProjectionBlocks

Gotsman--Linial: ProjectionBlocks #

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

Matrix blocks of a finite orthogonal projection family #

The Hilbert--Schmidt quantity below is the explicit sum of squared entry norms rather than an ambient matrix norm instance.

structure Complexity.BooleanAnalysis.PolynomialThreshold.Internal.OrthogonalProjectionFamily {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] (P : κ → Matrix ι ι ℂ) :

A finite orthogonal decomposition of the identity by Hermitian projections.

selfAdjoint (k : κ) : IsSelfAdjoint (P k)
idempotent (k : κ) : P k * P k = P k
orthogonal (r s : κ) : r ≠ s → P r * P s = 0
sum_eq_one : ∑ k : κ, P k = 1

Instances For

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.OrthogonalProjectionFamily.conjTranspose_eq {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] {P : κ → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (k : κ) :

(P k).conjTranspose = P k

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.OrthogonalProjectionFamily.mul_eq_ite {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] {P : κ → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) [DecidableEq κ] (r s : κ) :

P r * P s = if r = s then P r else 0

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sum_projection_blocks {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] {P : κ → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (B : Matrix ι ι ℂ) :

∑ r : κ, ∑ s : κ, P s * B * P r = B

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.projection_block_ext {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] {P : κ → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) {A B : Matrix ι ι ℂ} (h : ∀ (r s : κ), P s * A * P r = P s * B * P r) :

A = B

def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.matrixGrading {ι : Type u_1} {κ : Type u_2} [Fintype κ] (P : κ → Matrix ι ι ℂ) (weight : κ → ℝ) :

Matrix ι ι ℂ

The real-valued spectral multiplier defined by the projection family.

Equations

Complexity.BooleanAnalysis.PolynomialThreshold.Internal.matrixGrading P weight = ∑ k : κ, ↑(weight k) • P k

Instances For

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.projection_mul_matrixGrading {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] {P : κ → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (weight : κ → ℝ) (s : κ) :

P s * matrixGrading P weight = ↑(weight s) • P s

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.matrixGrading_mul_projection {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] {P : κ → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (weight : κ → ℝ) (r : κ) :

matrixGrading P weight * P r = ↑(weight r) • P r

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.projection_commutator {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] {P : κ → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (weight : κ → ℝ) (B : Matrix ι ι ℂ) (r s : κ) :

P s * (matrixGrading P weight * B - B * matrixGrading P weight) * P r = ↑(weight s - weight r) • (P s * B * P r)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.projection_anticommutator {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] {P : κ → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (weight : κ → ℝ) (B : Matrix ι ι ℂ) (r s : κ) :

P s * (matrixGrading P weight * B + B * matrixGrading P weight) * P r = ↑(weight s + weight r) • (P s * B * P r)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.trace_projection_sandwich {ι : Type u_1} [Fintype ι] (Q A : Matrix ι ι ℂ) (hQ : Q * Q = Q) :

(Q * A * Q).trace = (Q * A).trace

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq_projection_mul {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] {P : κ → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (s : κ) (B : Matrix ι ι ℂ) :

hsNormSq (P s * B) = (B.conjTranspose * P s * B).trace.re

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq_mul_projection {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] {P : κ → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (r : κ) (B : Matrix ι ι ℂ) :

hsNormSq (B * P r) = (P r * (B.conjTranspose * B)).trace.re

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq_left_projection_decomposition {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] {P : κ → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (B : Matrix ι ι ℂ) :

hsNormSq B = ∑ s : κ, hsNormSq (P s * B)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq_right_projection_decomposition {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] {P : κ → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (B : Matrix ι ι ℂ) :

hsNormSq B = ∑ r : κ, hsNormSq (B * P r)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq_block_parseval {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] {P : κ → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (B : Matrix ι ι ℂ) :

hsNormSq B = ∑ r : κ, ∑ s : κ, hsNormSq (P s * B * P r)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq_matrixGrading {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] {P : κ → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (weight : κ → ℝ) :

hsNormSq (matrixGrading P weight) = ∑ r : κ, weight r ^ 2 * hsNormSq (P r)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq_matrixGrading_trace {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] {P : κ → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (weight : κ → ℝ) :

hsNormSq (matrixGrading P weight) = ∑ r : κ, weight r ^ 2 * (P r).trace.re

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sum_hsNormSq_blocks_column {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] {P : κ → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (B : Matrix ι ι ℂ) (r : κ) (hB : B.conjTranspose * B = 1) :

∑ s : κ, hsNormSq (P s * B * P r) = hsNormSq (P r)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sum_hsNormSq_blocks_row {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] {P : κ → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (B : Matrix ι ι ℂ) (s : κ) (hB : B * B.conjTranspose = 1) :

∑ r : κ, hsNormSq (P s * B * P r) = hsNormSq (P s)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sum_hsNormSq_blocks_column_trace {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] {P : κ → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (B : Matrix ι ι ℂ) (r : κ) (hB : B.conjTranspose * B = 1) :

∑ s : κ, hsNormSq (P s * B * P r) = (P r).trace.re

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sum_hsNormSq_blocks_row_trace {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] {P : κ → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (B : Matrix ι ι ℂ) (s : κ) (hB : B * B.conjTranspose = 1) :

∑ r : κ, hsNormSq (P s * B * P r) = (P s).trace.re

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq_commutator {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] {P : κ → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (weight : κ → ℝ) (B : Matrix ι ι ℂ) :

hsNormSq (matrixGrading P weight * B - B * matrixGrading P weight) = ∑ r : κ, ∑ s : κ, (weight s - weight r) ^ 2 * hsNormSq (P s * B * P r)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq_anticommutator {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] {P : κ → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (weight : κ → ℝ) (B : Matrix ι ι ℂ) :

hsNormSq (matrixGrading P weight * B + B * matrixGrading P weight) = ∑ r : κ, ∑ s : κ, (weight s + weight r) ^ 2 * hsNormSq (P s * B * P r)

def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.degreeGrading {ι : Type u_1} {n : ℕ} (P : Fin (n + 1) → Matrix ι ι ℂ) :

Matrix ι ι ℂ

The degree grading associated to projections indexed from zero to n.

Equations

Complexity.BooleanAnalysis.PolynomialThreshold.Internal.degreeGrading P = Complexity.BooleanAnalysis.PolynomialThreshold.Internal.matrixGrading P fun (k : Fin (n + 1)) => ↑↑k

Instances For

noncomputable def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.centeredGrading {ι : Type u_1} {n : ℕ} (P : Fin (n + 1) → Matrix ι ι ℂ) :

Matrix ι ι ℂ

The degree grading centered at n / 2.

Equations

Complexity.BooleanAnalysis.PolynomialThreshold.Internal.centeredGrading P = Complexity.BooleanAnalysis.PolynomialThreshold.Internal.matrixGrading P fun (k : Fin (n + 1)) => ↑↑k - ↑n / 2

Instances For

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq_centeredGrading {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} {P : Fin (n + 1) → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) :

hsNormSq (centeredGrading P) = ∑ k : Fin (n + 1), (↑↑k - ↑n / 2) ^ 2 * hsNormSq (P k)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq_centeredGrading_trace {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} {P : Fin (n + 1) → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) :

hsNormSq (centeredGrading P) = ∑ k : Fin (n + 1), (↑↑k - ↑n / 2) ^ 2 * (P k).trace.re

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.centeredGrading_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} {P : Fin (n + 1) → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) :

centeredGrading P = degreeGrading P - ↑(↑n / 2) • 1

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.projection_centered_anticommutator {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} {P : Fin (n + 1) → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (B : Matrix ι ι ℂ) (r s : Fin (n + 1)) :

P s * (centeredGrading P * B + B * centeredGrading P) * P r = ↑(↑↑s + ↑↑r - ↑n) • (P s * B * P r)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq_centered_anticommutator {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} {P : Fin (n + 1) → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (B : Matrix ι ι ℂ) :

hsNormSq (centeredGrading P * B + B * centeredGrading P) = ∑ r : Fin (n + 1), ∑ s : Fin (n + 1), (↑↑s + ↑↑r - ↑n) ^ 2 * hsNormSq (P s * B * P r)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.instCompleteSpace_complexitylib {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] :

CompleteSpace E

noncomputable def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.operatorMatrixEquiv {ι : Type u_1} [Fintype ι] [DecidableEq ι] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (b : OrthonormalBasis ι ℂ E) :

(E →L[ℂ ] E) ≃ₐ[ℂ ] Matrix ι ι ℂ

Matrix representation of a continuous operator in an orthonormal basis, bundled with its algebraic compatibility.

Equations

Complexity.BooleanAnalysis.PolynomialThreshold.Internal.operatorMatrixEquiv b = (Module.End.toContinuousLinearMap E).symm.trans (LinearMap.toMatrixOrthonormal b).toAlgEquiv

Instances For

noncomputable def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.operatorMatrix {ι : Type u_1} [Fintype ι] [DecidableEq ι] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (b : OrthonormalBasis ι ℂ E) (T : E →L[ℂ ] E) :

Matrix ι ι ℂ

Matrix entries for the counting orthonormal basis or any chosen orthonormal basis.

Equations

Complexity.BooleanAnalysis.PolynomialThreshold.Internal.operatorMatrix b T = (Complexity.BooleanAnalysis.PolynomialThreshold.Internal.operatorMatrixEquiv b) T

Instances For

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.operatorMatrix_eq_toMatrix {ι : Type u_1} [Fintype ι] [DecidableEq ι] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (b : OrthonormalBasis ι ℂ E) (T : E →L[ℂ ] E) :

operatorMatrix b T = (LinearMap.toMatrixOrthonormal b) ↑T

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.operatorMatrix_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (b : OrthonormalBasis ι ℂ E) (T : E →L[ℂ ] E) (i j : ι) :

operatorMatrix b T i j = inner ℂ (b i) (T (b j))

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.operatorMatrix_injective {ι : Type u_1} [Fintype ι] [DecidableEq ι] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (b : OrthonormalBasis ι ℂ E) :

Function.Injective (operatorMatrix b)

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.operatorMatrix_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (b : OrthonormalBasis ι ℂ E) :

operatorMatrix b 0 = 0

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.operatorMatrix_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (b : OrthonormalBasis ι ℂ E) :

operatorMatrix b 1 = 1

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.operatorMatrix_add {ι : Type u_1} [Fintype ι] [DecidableEq ι] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (b : OrthonormalBasis ι ℂ E) (A B : E →L[ℂ ] E) :

operatorMatrix b (A + B) = operatorMatrix b A + operatorMatrix b B

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.operatorMatrix_sub {ι : Type u_1} [Fintype ι] [DecidableEq ι] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (b : OrthonormalBasis ι ℂ E) (A B : E →L[ℂ ] E) :

operatorMatrix b (A - B) = operatorMatrix b A - operatorMatrix b B

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.operatorMatrix_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (b : OrthonormalBasis ι ℂ E) (A B : E →L[ℂ ] E) :

operatorMatrix b (A * B) = operatorMatrix b A * operatorMatrix b B

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.operatorMatrix_smul {ι : Type u_1} [Fintype ι] [DecidableEq ι] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (b : OrthonormalBasis ι ℂ E) (z : ℂ) (T : E →L[ℂ ] E) :

operatorMatrix b (z • T) = z • operatorMatrix b T

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.operatorMatrix_sum {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (b : OrthonormalBasis ι ℂ E) (T : κ → E →L[ℂ ] E) :

operatorMatrix b (∑ k : κ, T k) = ∑ k : κ, operatorMatrix b (T k)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.operatorMatrix_isSelfAdjoint {ι : Type u_1} [Fintype ι] [DecidableEq ι] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (b : OrthonormalBasis ι ℂ E) (T : E →L[ℂ ] E) (hT : IsSelfAdjoint T) :

IsSelfAdjoint (operatorMatrix b T)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.orthogonalProjectionFamily_operatorMatrix {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (b : OrthonormalBasis ι ℂ E) (T : κ → E →L[ℂ ] E) (hself : ∀ (k : κ), IsSelfAdjoint (T k)) (hidem : ∀ (k : κ), T k * T k = T k) (horth : ∀ (r s : κ), r ≠ s → T r * T s = 0) (hsum : ∑ k : κ, T k = 1) :

OrthogonalProjectionFamily fun (k : κ) => operatorMatrix b (T k)

Transfer an actually constructed orthogonal family of Hilbert-space projections to the matrix interface used by the block estimates.

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.operatorMatrix_toEuclideanCLM {ι : Type u_1} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι ℂ) :

operatorMatrix (EuclideanSpace.basisFun ι ℂ) (Matrix.toEuclideanCLM A) = A

The standard-basis matrix representation is inverse to the standard Euclidean continuous linear operator associated to a matrix.