Gotsman--Linial: CoordinateMultipliers

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

Actual diagonal sign and coordinate operators on the cube

The matrices here act on the cube with its counting inner product. Their continuous linear maps act on EuclideanSpace, so all operator-norm statements refer to the intended Euclidean norm. The Hilbert--Schmidt statements use the explicit squared-entry sum hsNormSq.

def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.signMatrix {n : ℕ} (h : Cube n → ℝ) : Matrix (Cube n) (Cube n) ℂ

Multiplication by a real function on the cube, represented in the point-mass basis.

Equations

• Complexity.BooleanAnalysis.PolynomialThreshold.Internal.signMatrix h = Matrix.diagonal fun (x : Complexity.BooleanAnalysis.PolynomialThreshold.Internal.Cube n) => ↑(h x)

def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.coordinateSignMatrix {n : ℕ} (i : Fin n) : Matrix (Cube n) (Cube n) ℂ

The actual cube coordinate-sign matrix Z_i.

Equations

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

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.signMatrix_apply {n : ℕ} (h : Cube n → ℝ) (x y : Cube n) : signMatrix h x y = if x = y then ↑(h x) else 0

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.signMatrix_apply_self {n : ℕ} (h : Cube n → ℝ) (x : Cube n) : signMatrix h x x = ↑(h x)

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.coordinateSignMatrix_apply {n : ℕ} (i : Fin n) (x y : Cube n) : coordinateSignMatrix i x y = if x = y then ↑(cubeCoord x i) else 0

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.signMatrix_conjTranspose {n : ℕ} (h : Cube n → ℝ) : (signMatrix h).conjTranspose = signMatrix h

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.signMatrix_star {n : ℕ} (h : Cube n → ℝ) : star (signMatrix h) = signMatrix h

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.signMatrix_isHermitian {n : ℕ} (h : Cube n → ℝ) : (signMatrix h).IsHermitian

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.signMatrix_mul_self {n : ℕ} (h : Cube n → ℝ) (hh : ∀ (x : Cube n), h x = 1 ∨ h x = -1) : signMatrix h * signMatrix h = 1

A sign-valued real diagonal is an involution.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.signMatrix_conjTranspose_mul {n : ℕ} (h : Cube n → ℝ) (hh : ∀ (x : Cube n), h x = 1 ∨ h x = -1) : (signMatrix h).conjTranspose * signMatrix h = 1

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.signMatrix_mul_conjTranspose {n : ℕ} (h : Cube n → ℝ) (hh : ∀ (x : Cube n), h x = 1 ∨ h x = -1) : signMatrix h * (signMatrix h).conjTranspose = 1

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.signMatrix_unitary {n : ℕ} (h : Cube n → ℝ) (hh : ∀ (x : Cube n), h x = 1 ∨ h x = -1) : signMatrix h ∈ Matrix.unitaryGroup (Cube n) ℂ

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.signMatrix_commute_diagonal {n : ℕ} (h : Cube n → ℝ) (d : Cube n → ℂ) : Commute (signMatrix h) (Matrix.diagonal d)

A real sign diagonal commutes with every complex diagonal weight.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.signMatrix_mul_diagonal_comm {n : ℕ} (h : Cube n → ℝ) (d : Cube n → ℂ) : signMatrix h * Matrix.diagonal d = Matrix.diagonal d * signMatrix h

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.signMatrix_mulVec {n : ℕ} (h : Cube n → ℝ) (v : Cube n → ℂ) (x : Cube n) : (signMatrix h).mulVec v x = ↑(h x) * v x

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq_signMatrix {n : ℕ} (h : Cube n → ℝ) (hh : ∀ (x : Cube n), h x = 1 ∨ h x = -1) : hsNormSq (signMatrix h) = 2 ^ n

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.coordinateSignMatrix_conjTranspose {n : ℕ} (i : Fin n) : (coordinateSignMatrix i).conjTranspose = coordinateSignMatrix i

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.coordinateSignMatrix_star {n : ℕ} (i : Fin n) : star (coordinateSignMatrix i) = coordinateSignMatrix i

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.coordinateSignMatrix_isHermitian {n : ℕ} (i : Fin n) : (coordinateSignMatrix i).IsHermitian

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.coordinateSignMatrix_mul_self {n : ℕ} (i : Fin n) : coordinateSignMatrix i * coordinateSignMatrix i = 1

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.coordinateSignMatrix_conjTranspose_mul {n : ℕ} (i : Fin n) : (coordinateSignMatrix i).conjTranspose * coordinateSignMatrix i = 1

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.coordinateSignMatrix_mul_conjTranspose {n : ℕ} (i : Fin n) : coordinateSignMatrix i * (coordinateSignMatrix i).conjTranspose = 1

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.coordinateSignMatrix_unitary {n : ℕ} (i : Fin n) : coordinateSignMatrix i ∈ Matrix.unitaryGroup (Cube n) ℂ

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.coordinateSignMatrix_commute_diagonal {n : ℕ} (i : Fin n) (d : Cube n → ℂ) : Commute (coordinateSignMatrix i) (Matrix.diagonal d)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.coordinateSignMatrix_mul_diagonal_comm {n : ℕ} (i : Fin n) (d : Cube n → ℂ) : coordinateSignMatrix i * Matrix.diagonal d = Matrix.diagonal d * coordinateSignMatrix i

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.coordinateSignMatrix_mulVec {n : ℕ} (i : Fin n) (v : Cube n → ℂ) (x : Cube n) : (coordinateSignMatrix i).mulVec v x = ↑(cubeCoord x i) * v x

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq_coordinateSignMatrix {n : ℕ} (i : Fin n) : hsNormSq (coordinateSignMatrix i) = 2 ^ n

noncomputable def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.signMultiplier {n : ℕ} (h : Cube n → ℝ) : EuclideanSpace ℂ (Cube n) →L[ℂ] EuclideanSpace ℂ (Cube n)

The same diagonal action on the counting-inner-product Euclidean space.

Equations

• Complexity.BooleanAnalysis.PolynomialThreshold.Internal.signMultiplier h = Matrix.toEuclideanCLM (Complexity.BooleanAnalysis.PolynomialThreshold.Internal.signMatrix h)

noncomputable def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.coordinateMultiplier {n : ℕ} (i : Fin n) : EuclideanSpace ℂ (Cube n) →L[ℂ] EuclideanSpace ℂ (Cube n)

The actual coordinate multiplier on Euclidean space.

Equations

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

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.toEuclideanCLM_signMatrix {n : ℕ} (h : Cube n → ℝ) : Matrix.toEuclideanCLM (signMatrix h) = signMultiplier h

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.toEuclideanCLM_coordinateSignMatrix {n : ℕ} (i : Fin n) : Matrix.toEuclideanCLM (coordinateSignMatrix i) = coordinateMultiplier i

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.signMultiplier_apply {n : ℕ} (h : Cube n → ℝ) (v : EuclideanSpace ℂ (Cube n)) (x : Cube n) : ((signMultiplier h) v).ofLp x = ↑(h x) * v.ofLp x

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.coordinateMultiplier_apply {n : ℕ} (i : Fin n) (v : EuclideanSpace ℂ (Cube n)) (x : Cube n) : ((coordinateMultiplier i) v).ofLp x = ↑(cubeCoord x i) * v.ofLp x

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.signMultiplier_isSelfAdjoint {n : ℕ} (h : Cube n → ℝ) : IsSelfAdjoint (signMultiplier h)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.coordinateMultiplier_isSelfAdjoint {n : ℕ} (i : Fin n) : IsSelfAdjoint (coordinateMultiplier i)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.signMultiplier_mul_self {n : ℕ} (h : Cube n → ℝ) (hh : ∀ (x : Cube n), h x = 1 ∨ h x = -1) : signMultiplier h * signMultiplier h = 1

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.coordinateMultiplier_mul_self {n : ℕ} (i : Fin n) : coordinateMultiplier i * coordinateMultiplier i = 1

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.norm_signMultiplier_apply {n : ℕ} (h : Cube n → ℝ) (hh : ∀ (x : Cube n), h x = 1 ∨ h x = -1) (v : EuclideanSpace ℂ (Cube n)) : ‖(signMultiplier h) v‖ = ‖v‖

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.norm_coordinateMultiplier_apply {n : ℕ} (i : Fin n) (v : EuclideanSpace ℂ (Cube n)) : ‖(coordinateMultiplier i) v‖ = ‖v‖

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.norm_signMultiplier_le_one {n : ℕ} (h : Cube n → ℝ) (hh : ∀ (x : Cube n), h x = 1 ∨ h x = -1) : ‖signMultiplier h‖ ≤ 1

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.norm_coordinateMultiplier_le_one {n : ℕ} (i : Fin n) : ‖coordinateMultiplier i‖ ≤ 1