Documentation

Complexitylib.BooleanAnalysis.PolynomialThreshold.Internal.HilbertSchmidt

Gotsman--Linial: HilbertSchmidt #

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

noncomputable def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (A : Matrix ι κ ℂ) :

The Hilbert--Schmidt norm squared for the counting inner product. This explicit entry sum does not use any norm instance on matrices.

Equations

Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq A = ∑ i : ι, ∑ j : κ, ‖A i j‖ ^ 2

Instances For

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

0 ≤ hsNormSq A

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq_zero {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] :

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq_smul {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (c : ℂ) (A : Matrix ι κ ℂ) :

hsNormSq (c • A) = ‖c‖ ^ 2 * hsNormSq A

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq_real_smul {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (c : ℝ) (A : Matrix ι κ ℂ) :

hsNormSq (↑c • A) = c ^ 2 * hsNormSq A

@[simp]

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

hsNormSq A.conjTranspose = hsNormSq A

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.ofReal_sq_norm (z : ℂ) :

↑(‖z‖ ^ 2) = star z * z

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.ofReal_sum_sq_norm_column {ι : Type u_1} {κ : Type u_2} [Fintype ι] (A : Matrix ι κ ℂ) (j : κ) :

↑(∑ i : ι, ‖A i j‖ ^ 2) = (A.conjTranspose * A) j j

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

↑(hsNormSq A) = (A.conjTranspose * A).trace

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

hsNormSq A = (A.conjTranspose * A).trace.re

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

hsNormSq A = ∑ j : κ, ∑ i : ι, ‖A i j‖ ^ 2

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sum_sq_norm_column_eq_re {ι : Type u_1} {κ : Type u_2} [Fintype ι] (A : Matrix ι κ ℂ) (j : κ) :

∑ i : ι, ‖A i j‖ ^ 2 = ((A.conjTranspose * A) j j).re

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq_mul_left_of_unitary {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq ι] (U : Matrix ι ι ℂ) (A : Matrix ι κ ℂ) (hU : U.conjTranspose * U = 1) :

hsNormSq (U * A) = hsNormSq A

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq_mul_right_of_unitary {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq κ] (A : Matrix ι κ ℂ) (U : Matrix κ κ ℂ) (hU : U * U.conjTranspose = 1) :

hsNormSq (A * U) = hsNormSq A

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq_diagonal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (d : ι → ℂ) :

hsNormSq (Matrix.diagonal d) = ∑ i : ι, ‖d i‖ ^ 2

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] :

hsNormSq 1 = ↑(Fintype.card ι)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq_of_unitary {ι : Type u_1} [Fintype ι] [DecidableEq ι] (U : Matrix ι ι ℂ) (hU : U.conjTranspose * U = 1) :

hsNormSq U = ↑(Fintype.card ι)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq_diagonal_of_norm_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (d : ι → ℂ) (hd : ∀ (i : ι), ‖d i‖ = 1) :

hsNormSq (Matrix.diagonal d) = ↑(Fintype.card ι)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq_projection {ι : Type u_1} [Fintype ι] (P : Matrix ι ι ℂ) (hself : P.conjTranspose = P) (hidem : P * P = P) :

hsNormSq P = P.trace.re

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sum_sq_norm_column_of_unitary {ι : Type u_1} [Fintype ι] [DecidableEq ι] (U : Matrix ι ι ℂ) (hU : U.conjTranspose * U = 1) (j : ι) :

∑ i : ι, ‖U i j‖ ^ 2 = 1

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sq_norm_entry_le_one_of_unitary {ι : Type u_1} [Fintype ι] [DecidableEq ι] (U : Matrix ι ι ℂ) (hU : U.conjTranspose * U = 1) (i j : ι) :

‖U i j‖ ^ 2 ≤ 1