Gotsman--Linial: ProjectionTrace

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

Traces of actual orthogonal projections

The trace calculation uses the algebraic theorem for a projection onto a submodule. In particular, no spectral decomposition or matrix norm instance is needed. Matrix transport is valid in every basis, and hence in the orthonormal basis used for the weighted grading.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.starProjection_isProj {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (K : Submodule 𝕜 E) : LinearMap.IsProj K ↑K.starProjection

The actual orthogonal projection is algebraically a projection onto its specified submodule.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.trace_starProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (K : Submodule 𝕜 E) : (LinearMap.trace 𝕜 E) ↑K.starProjection = ↑(Module.finrank 𝕜 ↥K)

The trace of the actual orthogonal projection is the dimension of its range.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.trace_toMatrix_starProjection {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [Fintype ι] [DecidableEq ι] (b : Module.Basis ι 𝕜 E) (K : Submodule 𝕜 E) : ((LinearMap.toMatrix b b) ↑K.starProjection).trace = ↑(Module.finrank 𝕜 ↥K)

The matrix trace of an orthogonal projection is independent of the chosen basis.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.trace_toMatrixOrthonormal_starProjection {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [Fintype ι] [DecidableEq ι] (b : OrthonormalBasis ι 𝕜 E) (K : Submodule 𝕜 E) : ((LinearMap.toMatrixOrthonormal b) ↑K.starProjection).trace = ↑(Module.finrank 𝕜 ↥K)

The orthonormal matrix representation used by the grading has the correct trace.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.re_trace_toMatrixOrthonormal_starProjection {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] [Fintype ι] [DecidableEq ι] (b : OrthonormalBasis ι ℂ E) (K : Submodule ℂ E) : ((LinearMap.toMatrixOrthonormal b) ↑K.starProjection).trace.re = ↑(Module.finrank ℂ ↥K)

The real trace required by Hilbert--Schmidt block-mass computations.