Correlation with quadratic forms through rectangles

The correlation of two sets of inputs S and T is the fraction of inputs on which membership in S and in T agree, minus the fraction on which it differs: in terms of the agreement of the frontier method, correlation S T = 2 · agreement S T - 1 (Cslib.Circuits.Frontier.correlation_eq_two_mul_agreement_sub_one). For Boolean functions f and g it is E[(-1)^{f + g}].

Quadratic forms are balanced on rectangles (sq_signedCount_quadForm_rectangle_mul_le). Let S be the set where the quadratic form of a matrix Q over 𝔽₂ is true, and cut the coordinates into X and Xᶜ. On an input glued from a part p on X and a part q off X, the form is a form in p, plus a form in q, plus the bilinear pairing p ⬝ᵥ C q of the block C of the polar matrix Q + Qᵀ with rows X and columns Xᶜ, whose rank is the cut rank ρ(X). Lindsey's lemma then bounds the signed count of S on every rectangle R for the cut X:

signedCount S R ² · 2^{ρ(X)} ≤ |R| · 2^n.

Correlation through rectangle classes (sq_correlation_quadForm_mul_le). Partition the inputs into classes on which membership in T is constant and each of which is a rectangle for the cut X. Lindsey's lemma on every class and Cauchy–Schwarz over the classes give

correlation S T ² · 2^{ρ(X)} ≤ #classes.

Main results

• Cslib.Circuits.Frontier.sq_signedCount_quadForm_rectangle_mul_le: quadratic forms are balanced on rectangles of large cut rank.
• Cslib.Circuits.Frontier.sq_correlation_quadForm_mul_le: correlation through rectangle classes.

References

• S. Jukna, Extremal Combinatorics, Ch. 14

Quadratic forms on rectangles

theorem Cslib.Circuits.Frontier.sq_signedCount_quadForm_rectangle_mul_le {ι : Type u_1} [Fintype ι] (Q : Matrix ι ι (ZMod 2)) (X : Set ι) (A : Set (↑X → Bool)) (B : Set (↑Xᶜ → Bool)) : signedCount {x : ι → Bool | BitString.quadForm Q x = true} (rectangle X A B) ^ 2 * 2 ^ (Q + Q.transpose).cutRank X ≤ ↑(rectangle X A B).ncard * 2 ^ Fintype.card ι

Quadratic forms are balanced on rectangles. Let S be the set where the quadratic form of Q over 𝔽₂ is true. On every rectangle R for the cut X, the signed count of S satisfies signedCount S R ² · 2^{ρ(X)} ≤ |R| · 2^n, where ρ(X) is the cut rank of the polar matrix Q + Qᵀ at X.

On an input glued from p on X and q off X, the sign of the form is the sign of a form in p, times the sign of a form in q, times the sign of the pairing of p and q through the block of Q + Qᵀ with rows X and columns Xᶜ; this is Lindsey's lemma for that block.

theorem Cslib.Circuits.Frontier.sq_correlation_quadForm_mul_le {ι : Type u_1} [Fintype ι] (Q : Matrix ι ι (ZMod 2)) (T : Set (ι → Bool)) {M : Type u_2} (msg : (ι → Bool) → M) (X : Set ι) (hT : ∀ (x y : ι → Bool), msg x = msg y → (x ∈ T ↔ y ∈ T)) (hrect : ∀ (x : ι → Bool), ∃ (A : Set (↑X → Bool)) (B : Set (↑Xᶜ → Bool)), {y : ι → Bool | msg y = msg x} = rectangle X A B) : correlation {x : ι → Bool | BitString.quadForm Q x = true} T ^ 2 * 2 ^ (Q + Q.transpose).cutRank X ≤ ↑(Set.range msg).ncard

Correlation through rectangle classes. Let S be the set where the quadratic form of Q over 𝔽₂ is true. Let membership in T be constant on the classes of msg, and let every class be a rectangle for the cut X. Then

correlation S T ² · 2^{ρ(X)} ≤ #classes,

where ρ(X) is the cut rank of the polar matrix Q + Qᵀ at X. This is Lindsey's lemma on each class and Cauchy–Schwarz over the classes.