Documentation

Complexitylib.Circuits.Correlation.Internal.Lindsey

Lindsey's lemma over GF(2) #

For a matrix B over ZMod 2 with rows indexed by α and columns by β, sets P and Q of vectors, and weights of absolute value at most one,

(∑_{p ∈ P} ∑_{q ∈ Q} g(p) h(q) (-1)^{p · B q})² · 2^{rank B} ≤ |P| |Q| 2^{|α|} 2^{|β|}.

This is Lindsey's lemma: a bilinear form of large rank is nearly balanced on every large rectangle. The proof is Cauchy–Schwarz over p, character orthogonality ∑_p (-1)^{p · v} = 2^{|α|} [v = 0], and the count |{q' : B q' = B q}| = 2^{|β| - rank B}.

source
def Complexity.Correlation.zsign (z : ZMod 2) :
ℝ

The sign (-1)^z of an element z of ZMod 2, as a real number.

Equations
Instances For
    source
    theorem Complexity.Correlation.zmod_two_eq_zero_or_one (z : ZMod 2) :
    z = 0 ∨ z = 1
    source
    theorem Complexity.Correlation.zmod_two_add_eq_zero_iff (a b : ZMod 2) :
    a + b = 0 ↔ b = a
    source
    theorem Complexity.Correlation.add_eq_zero_iff_eq_zmod_two {γ : Type u_3} (u v : γ → ZMod 2) :
    u + v = 0 ↔ v = u

    Over ZMod 2, two vectors sum to zero exactly when they are equal.

    source
    theorem Complexity.Correlation.zsign_add (a b : ZMod 2) :
    zsign (a + b) = zsign a * zsign b
    source
    theorem Complexity.Correlation.zsign_add_one (a : ZMod 2) :
    zsign (a + 1) = -zsign a
    source
    @[simp]
    theorem Complexity.Correlation.abs_zsign (z : ZMod 2) :
    |zsign z| = 1
    source
    @[simp]
    theorem Complexity.Correlation.zsign_sq (z : ZMod 2) :
    zsign z ^ 2 = 1
    source
    theorem Complexity.Correlation.sum_zsign_dotProduct {α : Type u_1} [Fintype α] [DecidableEq α] (v : α → ZMod 2) :
    ∑ p : α → ZMod 2, zsign (p ⬝ᵥ v) = if v = 0 then 2 ^ Fintype.card α else 0

    Character orthogonality. The signs (-1)^{p · v} cancel over all p unless v = 0.

    source
    theorem Complexity.Correlation.card_filter_mulVec_eq {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq β] (B : Matrix α β (ZMod 2)) (q : β → ZMod 2) :
    {z : β → ZMod 2 | B.mulVec z = B.mulVec q}.card = {z : β → ZMod 2 | B.mulVec z = 0}.card

    All fibres of a linear map have the size of its kernel.

    source
    theorem Complexity.Correlation.card_ker_mul_two_pow_rank {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq β] (B : Matrix α β (ZMod 2)) :
    {z : β → ZMod 2 | B.mulVec z = 0}.card * 2 ^ B.rank = 2 ^ Fintype.card β

    The kernel of B has 2^{|β| - rank B} elements.

    source
    theorem Complexity.Correlation.sq_sum_bilinear_mul_two_pow_rank_le {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (B : Matrix α β (ZMod 2)) (P : Finset (α → ZMod 2)) (Q : Finset (β → ZMod 2)) (g : (α → ZMod 2) → ℝ) (h : (β → ZMod 2) → ℝ) (hg : ∀ (p : α → ZMod 2), |g p| ≤ 1) (hh : ∀ (q : β → ZMod 2), |h q| ≤ 1) :
    (∑ p ∈ P, ∑ q ∈ Q, g p * h q * zsign (p ⬝ᵥ B.mulVec q)) ^ 2 * 2 ^ B.rank ≤ ↑P.card * ↑Q.card * 2 ^ Fintype.card α * 2 ^ Fintype.card β

    Lindsey's lemma over GF(2).