Gotsman--Linial: BlockCoupling

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/BlockCoupling.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 finite block coupling

Normalize a nonnegative matrix of block masses, identify its two binomial marginals, and reflect its first index. The low-degree block vanishing gives the one-sided displacement bound required by the finite coupling lemma.

noncomputable def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.normalizedPairWeight {α : Type u_1} {β : Type u_2} (B : α → β → ℝ) (Z : ℝ) (t : α × β) : ℝ

Normalize finite two-index masses by their total mass.

Equations

• Complexity.BooleanAnalysis.PolynomialThreshold.Internal.normalizedPairWeight B Z t = B t.1 t.2 / Z

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.normalizedPairWeight_nonneg {α : Type u_1} {β : Type u_2} (B : α → β → ℝ) (Z : ℝ) (hB : ∀ (r : α) (s : β), 0 ≤ B r s) (hZ : 0 ≤ Z) (t : α × β) : 0 ≤ normalizedPairWeight B Z t

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.normalizedPairWeight_row {α : Type u_1} {β : Type u_2} [Fintype β] (B : α → β → ℝ) (Z : ℝ) (r : α) : ∑ s : β, normalizedPairWeight B Z (r, s) = (∑ s : β, B r s) / Z

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.normalizedPairWeight_column {α : Type u_1} {β : Type u_2} [Fintype α] (B : α → β → ℝ) (Z : ℝ) (s : β) : ∑ r : α, normalizedPairWeight B Z (r, s) = (∑ r : α, B r s) / Z

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.normalizedPairWeight_expect_fst {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (B : α → β → ℝ) (Z : ℝ) (φ : α → ℝ) : ∑ t : α × β, normalizedPairWeight B Z t * φ t.1 = ∑ r : α, (∑ s : β, B r s) / Z * φ r

First-coordinate expectations are computed from the row sums.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.normalizedPairWeight_expect_snd {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (B : α → β → ℝ) (Z : ℝ) (φ : β → ℝ) : ∑ t : α × β, normalizedPairWeight B Z t * φ t.2 = ∑ s : β, (∑ r : α, B r s) / Z * φ s

Second-coordinate expectations are computed from the column sums.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.binomial_block_coupling_bound (n d : ℕ) (B : Fin (n + 1) → Fin (n + 1) → ℝ) (hB : ∀ (r s : Fin (n + 1)), 0 ≤ B r s) (hrow : ∀ (r : Fin (n + 1)), ∑ s : Fin (n + 1), B r s = ↑(n.choose ↑r)) (hcol : ∀ (s : Fin (n + 1)), ∑ r : Fin (n + 1), B r s = ↑(n.choose ↑s)) (hvanish : ∀ (r s : Fin (n + 1)), ↑r + ↑s < n - d → B r s = 0) : ∑ r : Fin (n + 1), ∑ s : Fin (n + 1), (↑↑s + ↑↑r - ↑n) ^ 2 * B r s ≤ 4 * ↑d * √↑n * 2 ^ n

Finite masses with binomial row and column sums, supported above the anti-diagonal r+s=n-d, have the required centered quadratic bound.

noncomputable def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.blockCouplingWeight {n : ℕ} {ι : Type u_1} [Fintype ι] (P : Fin (n + 1) → Matrix ι ι ℂ) (H : Matrix ι ι ℂ) (t : Fin (n + 1) × Fin (n + 1)) : ℝ

The actual finite probability weights supplied by the Hilbert--Schmidt blocks of an operator in a binomial orthogonal grading.

Equations

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

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.blockCouplingWeight_nonneg {n : ℕ} {ι : Type u_1} [Fintype ι] (P : Fin (n + 1) → Matrix ι ι ℂ) (H : Matrix ι ι ℂ) (t : Fin (n + 1) × Fin (n + 1)) : 0 ≤ blockCouplingWeight P H t

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.blockCouplingWeight_fst_marginal {n : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] {P : Fin (n + 1) → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (H : Matrix ι ι ℂ) (hH : H.conjTranspose * H = 1) (hmult : ∀ (k : Fin (n + 1)), hsNormSq (P k) = ↑(n.choose ↑k)) (r : Fin (n + 1)) : ∑ s : Fin (n + 1), blockCouplingWeight P H (r, s) = binomialWeight n r

The first block index has the binomial distribution.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.blockCouplingWeight_snd_marginal {n : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] {P : Fin (n + 1) → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (H : Matrix ι ι ℂ) (hH : H * H.conjTranspose = 1) (hmult : ∀ (k : Fin (n + 1)), hsNormSq (P k) = ↑(n.choose ↑k)) (s : Fin (n + 1)) : ∑ r : Fin (n + 1), blockCouplingWeight P H (r, s) = binomialWeight n s

The second block index has the same binomial distribution.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sum_blockCouplingWeight {n : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] {P : Fin (n + 1) → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (H : Matrix ι ι ℂ) (hH : H.conjTranspose * H = 1) (hmult : ∀ (k : Fin (n + 1)), hsNormSq (P k) = ↑(n.choose ↑k)) : ∑ t : Fin (n + 1) × Fin (n + 1), blockCouplingWeight P H t = 1

Unitarity and the grading multiplicities make the block weights a probability distribution without any additional normalization assumption.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.blockCouplingWeight_support {n d : ℕ} {ι : Type u_1} [Fintype ι] (P : Fin (n + 1) → Matrix ι ι ℂ) (H : Matrix ι ι ℂ) (hvanish : ∀ (r s : Fin (n + 1)), ↑r + ↑s < n - d → P s * H * P r = 0) (r s : Fin (n + 1)) (ht : blockCouplingWeight P H (r, s) ≠ 0) : n - d ≤ ↑r + ↑s

A nonzero block probability lies on or above the required anti-diagonal.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq_centeredGrading_anticommutator_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (n d : ℕ) (P : Fin (n + 1) → Matrix ι ι ℂ) (hP : OrthogonalProjectionFamily P) (H : Matrix ι ι ℂ) (hleft : H.conjTranspose * H = 1) (hright : H * H.conjTranspose = 1) (hmult : ∀ (k : Fin (n + 1)), hsNormSq (P k) = ↑(n.choose ↑k)) (hvanish : ∀ (r s : Fin (n + 1)), ↑r + ↑s < n - d → P s * H * P r = 0) : hsNormSq (centeredGrading P * H + H * centeredGrading P) ≤ 4 * ↑d * √↑n * 2 ^ n

The spectral block coupling bounds the actual centered grading anticommutator. Its hypotheses are the orthogonal grading, its binomial multiplicities, unitarity, and the separately proved low-degree vanishing.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq_centeredGrading_anticommutator_le_of_trace {ι : Type u_1} [Fintype ι] [DecidableEq ι] (n d : ℕ) (P : Fin (n + 1) → Matrix ι ι ℂ) (hP : OrthogonalProjectionFamily P) (H : Matrix ι ι ℂ) (hleft : H.conjTranspose * H = 1) (hright : H * H.conjTranspose = 1) (htrace : ∀ (k : Fin (n + 1)), (P k).trace.re = ↑(n.choose ↑k)) (hvanish : ∀ (r s : Fin (n + 1)), ↑r + ↑s < n - d → P s * H * P r = 0) : hsNormSq (centeredGrading P * H + H * centeredGrading P) ≤ 4 * ↑d * √↑n * 2 ^ n

Trace-multiplicity form, for direct use with finite-dimensional orthogonal projections whose ranks have already been computed.