Quadratic forms are balanced on rectangles of large cut rank

Cut the coordinates into X and Xᶜ. On an input glued from an X-part p and an Xᶜ-part q, the quadratic form of Q is a function of p, plus a function of q, plus p · B q for the block B of Q + Qᵀ with rows X and columns Xᶜ. Lindsey's lemma then bounds the signed sum of the form over every rectangle R for the cut X:

(∑_{x ∈ R} (-1)^{f(x)})² · 2^{cutRank Q X} ≤ |R| · 2^n.

theorem Complexity.Correlation.bit_injective : Function.Injective bit

theorem Complexity.Correlation.boolSign_quadForm {ι : Type u_1} [Fintype ι] (Q : Matrix ι ι (ZMod 2)) (x : ι → Bool) : Frontier.boolSign (quadForm Q x) = -zsign (∑ i : ι, ∑ j : ι, Q i j * bit (x i) * bit (x j))

The sign of a quadratic form is the negated sign of its value in ZMod 2.

def Complexity.Correlation.merge {ι : Type u_1} (X : Set ι) [DecidablePred fun (x : ι) => x ∈ X] {γ : Type u_2} (p : ↑X → γ) (q : ↑Xᶜ → γ) : ι → γ

The input whose part on X is p and whose part on Xᶜ is q.

Equations

• Complexity.Correlation.merge X p q i = if h : i ∈ X then p ⟨i, h⟩ else q ⟨i, h⟩

@[simp]

theorem Complexity.Correlation.merge_coe_left {ι : Type u_1} {X : Set ι} [DecidablePred fun (x : ι) => x ∈ X] {γ : Type u_2} (p : ↑X → γ) (q : ↑Xᶜ → γ) (i : ↑X) : merge X p q ↑i = p i

@[simp]

theorem Complexity.Correlation.merge_coe_right {ι : Type u_1} {X : Set ι} [DecidablePred fun (x : ι) => x ∈ X] {γ : Type u_2} (p : ↑X → γ) (q : ↑Xᶜ → γ) (i : ↑Xᶜ) : merge X p q ↑i = q i

theorem Complexity.Correlation.domRestrict_merge {ι : Type u_1} {X : Set ι} [DecidablePred fun (x : ι) => x ∈ X] {γ : Type u_2} (p : ↑X → γ) (q : ↑Xᶜ → γ) : X.domRestrict (merge X p q) = p

theorem Complexity.Correlation.domRestrict_compl_merge {ι : Type u_1} {X : Set ι} [DecidablePred fun (x : ι) => x ∈ X] {γ : Type u_2} (p : ↑X → γ) (q : ↑Xᶜ → γ) : Xᶜ.domRestrict (merge X p q) = q

theorem Complexity.Correlation.merge_domRestrict {ι : Type u_1} {X : Set ι} [DecidablePred fun (x : ι) => x ∈ X] {γ : Type u_2} (x : ι → γ) : merge X (X.domRestrict x) (Xᶜ.domRestrict x) = x

theorem Complexity.Correlation.comp_merge {ι : Type u_1} {X : Set ι} [DecidablePred fun (x : ι) => x ∈ X] {γ : Type u_2} {δ : Type u_3} (f : γ → δ) (p : ↑X → γ) (q : ↑Xᶜ → γ) : f ∘ merge X p q = merge X (f ∘ p) (f ∘ q)

theorem Complexity.Correlation.sum_eq_sum_add_sum_compl {ι : Type u_1} {X : Set ι} [DecidablePred fun (x : ι) => x ∈ X] [Fintype ι] [Fintype ↑X] [Fintype ↑Xᶜ] {M : Type u_2} [AddCommMonoid M] (f : ι → M) : ∑ i : ι, f i = ∑ i : ↑X, f ↑i + ∑ i : ↑Xᶜ, f ↑i

A sum over all coordinates splits into the coordinates of X and of Xᶜ.

theorem Complexity.Correlation.sum_eq_sum_sum_merge {ι : Type u_1} {X : Set ι} [DecidablePred fun (x : ι) => x ∈ X] {γ : Type u_2} {s : Finset (ι → γ)} {A : Finset (↑X → γ)} {B : Finset (↑Xᶜ → γ)} (hs : ∀ (x : ι → γ), x ∈ s ↔ X.domRestrict x ∈ A ∧ Xᶜ.domRestrict x ∈ B) (w : (ι → γ) → ℝ) : ∑ x ∈ s, w x = ∑ p ∈ A, ∑ q ∈ B, w (merge X p q)

A sum over a rectangle is a double sum over its two sides.

def Complexity.Correlation.cutMatrix {ι : Type u_1} (Q : Matrix ι ι (ZMod 2)) (X : Set ι) : Matrix (↑X) (↑Xᶜ) (ZMod 2)

The block of the polar matrix Q + Qᵀ with rows X and columns Xᶜ.

Equations

• Complexity.Correlation.cutMatrix Q X i j = Q ↑i ↑j + Q ↑j ↑i

theorem Complexity.Correlation.rank_cutMatrix {ι : Type u_1} {X : Set ι} [Fintype ↑Xᶜ] [Finite ι] (Q : Matrix ι ι (ZMod 2)) : (cutMatrix Q X).rank = cutRank Q X

theorem Complexity.Correlation.quad_merge {ι : Type u_1} {X : Set ι} [DecidablePred fun (x : ι) => x ∈ X] [Fintype ι] [Fintype ↑X] [Fintype ↑Xᶜ] (Q : Matrix ι ι (ZMod 2)) (u : ↑X → ZMod 2) (v : ↑Xᶜ → ZMod 2) : ∑ i : ι, ∑ j : ι, Q i j * merge X u v i * merge X u v j = ∑ i : ↑X, ∑ j : ↑X, Q ↑i ↑j * u i * u j + ∑ i : ↑Xᶜ, ∑ j : ↑Xᶜ, Q ↑i ↑j * v i * v j + u ⬝ᵥ (cutMatrix Q X).mulVec v

The polarization of a quadratic form across a cut.

theorem Complexity.Correlation.sq_sum_boolSign_quadForm_mul_le {ι : Type u_1} {X : Set ι} [DecidablePred fun (x : ι) => x ∈ X] [Fintype ι] [DecidableEq ι] (Q : Matrix ι ι (ZMod 2)) {s : Finset (ι → Bool)} {A : Finset (↑X → Bool)} {B : Finset (↑Xᶜ → Bool)} (hs : ∀ (x : ι → Bool), x ∈ s ↔ X.domRestrict x ∈ A ∧ Xᶜ.domRestrict x ∈ B) : (∑ x ∈ s, Frontier.boolSign (quadForm Q x)) ^ 2 * 2 ^ cutRank Q X ≤ ↑s.card * 2 ^ Fintype.card ι

Lindsey's lemma for quadratic forms. Over any rectangle s for the cut X, the signed sum of the quadratic form of Q satisfies (∑_s (-1)^f)² · 2^{cutRank Q X} ≤ |s| 2^n.