Quadratic forms over GF(2) and their ranks -- definitions

The hard functions of the correlation bounds are quadratic forms over the field with two elements. An input x : ι → Bool is read coordinatewise as a vector over ZMod 2 (Correlation.bit), and a square matrix Q defines the Boolean function x ↦ ∑ i, ∑ j, Q i j x_i x_j (Correlation.quadForm). Only the polar matrix Q + Qᵀ matters for correlation with circuits: cutting the coordinates into U and Uᶜ, the form is a function of the U-part, plus a function of the Uᶜ-part, plus the bilinear pairing of the two parts through the block of Q + Qᵀ with rows U and columns Uᶜ. The rank of that block is the cut rank of Q at U (Correlation.cutRank).

Ranks of blocks are the dimension over ZMod 2 of the span of their rows (Correlation.blockRank); this needs no Fintype instance on the index sets. A matrix is submatrix-robust with deficiency t (Correlation.SubmatrixRobust) when every square block with k rows has rank at least k - t.

The explicit family is a bilinear form xᵀ R y (Correlation.bilinForm): on inputs of length n the left half x consists of the first ⌊n/2⌋ coordinates, the right half y of the next ⌊n/2⌋, and for odd n the last coordinate is ignored.

Main definitions

• Correlation.bit, Correlation.quadForm: a quadratic form as a Boolean function.
• Correlation.blockRank, Correlation.cutRank: ranks of blocks and cut ranks.
• Correlation.SubmatrixRobust: every square block is nearly of full rank.
• Correlation.leftIdx, Correlation.rightIdx, Correlation.bilinForm: the bilinear form xᵀ R y on inputs of length n.

noncomputable def Complexity.Correlation.correlation {α : Type u_3} (f g : α → Bool) : ℝ

The correlation of two Boolean functions on a finite domain: |Pr[f = g] - Pr[f ≠ g]| = |2 · agreement f g - 1|.

Equations

• Complexity.Correlation.correlation f g = |2 * Complexity.Frontier.agreement f g - 1|

def Complexity.Correlation.bit (b : Bool) : ZMod 2

A bit read as 0 or 1 in ZMod 2.

Equations

• Complexity.Correlation.bit b = if b = true then 1 else 0

def Complexity.Correlation.quadForm {ι : Type u_1} [Fintype ι] (Q : Matrix ι ι (ZMod 2)) (x : ι → Bool) : Bool

The quadratic form of a square matrix Q over GF(2), as a Boolean function: an input x is mapped to ∑ i, ∑ j, Q i j x_i x_j.

Equations

• Complexity.Correlation.quadForm Q x = decide (∑ i : ι, ∑ j : ι, Q i j * Complexity.Correlation.bit (x i) * Complexity.Correlation.bit (x j) = 1)

noncomputable def Complexity.Correlation.blockRank {ι : Type u_1} {κ : Type u_2} (M : Matrix ι κ (ZMod 2)) (S : Set ι) (T : Set κ) : ℕ

The rank over GF(2) of the block of M with rows S and columns T: the dimension of the span of its rows, each a vector indexed by T.

Equations

• Complexity.Correlation.blockRank M S T = Module.finrank (ZMod 2) ↥(Submodule.span (ZMod 2) (Set.range fun (i : ↑S) (j : ↑T) => M ↑i ↑j))

noncomputable def Complexity.Correlation.cutRank {ι : Type u_1} (Q : Matrix ι ι (ZMod 2)) (U : Set ι) : ℕ

The cut rank of Q at U: the rank of the block of the polar matrix Q + Qᵀ with rows U and columns Uᶜ. For a symmetric zero-diagonal matrix, the adjacency matrix of a graph, this is the cut rank of U in the graph.

Equations

• Complexity.Correlation.cutRank Q U = Complexity.Correlation.blockRank (Q + Q.transpose) U Uᶜ

def Complexity.Correlation.SubmatrixRobust {ι : Type u_1} {κ : Type u_2} (R : Matrix ι κ (ZMod 2)) (t : ℕ) : Prop

R is submatrix-robust with deficiency t: every square block of R, with k rows and k columns, has rank at least k - t.

Equations

• Complexity.Correlation.SubmatrixRobust R t = ∀ (S : Set ι) (T : Set κ), S.ncard = T.ncard → S.ncard ≤ Complexity.Correlation.blockRank R S T + t

def Complexity.Correlation.robustDeficiency (m : ℕ) : ℕ

The deficiency 2 ⌊√m⌋ + 1: submatrix-robust m × m matrices with this deficiency exist (Correlation.exists_submatrixRobust).

Equations

• Complexity.Correlation.robustDeficiency m = 2 * m.sqrt + 1

def Complexity.Correlation.leftIdx (n : ℕ) (a : Fin (n / 2)) : Fin n

The coordinate of an input of length n that holds the entry a of its left half.

Equations

• Complexity.Correlation.leftIdx n a = ⟨↑a, ⋯⟩

def Complexity.Correlation.rightIdx (n : ℕ) (b : Fin (n / 2)) : Fin n

The coordinate of an input of length n that holds the entry b of its right half.

Equations

• Complexity.Correlation.rightIdx n b = ⟨n / 2 + ↑b, ⋯⟩

def Complexity.Correlation.bilinForm {n : ℕ} (R : Matrix (Fin (n / 2)) (Fin (n / 2)) (ZMod 2)) (x : Fin n → Bool) : Bool

The bilinear form xᵀ R y on inputs of length n, where x is the left half (the first ⌊n/2⌋ coordinates) and y the right half (the next ⌊n/2⌋). For odd n the last coordinate is ignored.

Equations

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

def Complexity.Correlation.bipartiteMatrix (n : ℕ) (R : Matrix (Fin (n / 2)) (Fin (n / 2)) (ZMod 2)) : Matrix (Fin n) (Fin n) (ZMod 2)

The n × n matrix with R in the block whose rows are the left half and whose columns are the right half, and zeros elsewhere.

Equations

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