Documentation

Complexity.Computability.PCP.Approximation.Hastad.LinearTest

Håstad's 3-Bit Linear Test and Spectral Decoding Weights #

This module formalizes Håstad's noisy 3-bit linear test on folded (odd, Cslib.BitString.IsOdd) Long Code tables over a single projection π : β → γ, its exact Walsh–Fourier expansion, and the Cauchy–Schwarz and Parseval soundness bound via low-degree spectral decoding weights [Has01]. The Long Code, folding and the mod-2 projection Cslib.BitString.projectSet live in Complexity.Foundations.BooleanAnalysis.LongCode.

Main definitions #

Main results #

References #

Håstad's 3-bit linear test and its Fourier expansion #

source
noncomputable def Cslib.PCP.Hastad.hastadLinearCorr {β : Type u_2} {γ : Type u_3} [Fintype β] [DecidableEq β] [Fintype γ] [DecidableEq γ] (π : β → γ) (δ : ℝ) (B : (γ → Bool) → Bool) (A : (β → Bool) → Bool) :
ℝ

The correlation of Håstad's 3-bit linear test on a projection π : β → γ at noise rate δ between tables B : (γ → Bool) → Bool and A : (β → Bool) → Bool Håstad, Section 5: the expected product of the ±1 signs of B f, A g, and A ((f ∘ π) + g + μ) over uniform f : γ → Bool, uniform g : β → Bool, and δ-biased Bernoulli noise μ : β → Bool.

Instances For
    source
    noncomputable def Cslib.PCP.Hastad.hastadLinearProb {β : Type u_2} {γ : Type u_3} [Fintype β] [DecidableEq β] [Fintype γ] [DecidableEq γ] (π : β → γ) (δ : ℝ) (B : (γ → Bool) → Bool) (A : (β → Bool) → Bool) :
    ℝ

    The acceptance probability of Håstad's 3-bit linear test: the probability that (B f ^^ A g ^^ A ((f ∘ π) + g + μ)) = false under uniform f, g and δ-biased noise μ.

    Instances For
      source
      theorem Cslib.PCP.Hastad.hastadLinearProb_eq_add_hastadLinearCorr {β : Type u_2} {γ : Type u_3} [Fintype β] [DecidableEq β] [Fintype γ] [DecidableEq γ] (π : β → γ) (δ : ℝ) (B : (γ → Bool) → Bool) (A : (β → Bool) → Bool) :
      hastadLinearProb π δ B A = 1 / 2 + 1 / 2 * hastadLinearCorr π δ B A

      The acceptance probability of Håstad's 3-bit linear test is 1 / 2 + 1 / 2 * hastadLinearCorr π δ B A.

      source
      theorem Cslib.PCP.Hastad.hastadLinearCorr_longCode {β : Type u_2} {γ : Type u_3} [Fintype β] [DecidableEq β] [Fintype γ] [DecidableEq γ] (π : β → γ) (δ : ℝ) (x : β) :
      hastadLinearCorr π δ (BitString.longCode (π x)) (BitString.longCode x) = 1 - 2 * δ

      Completeness of Håstad's 3-bit linear test (correlation): on matching Long Code tables longCode (π x) and longCode x, the correlation is 1 - 2 * δ.

      source
      theorem Cslib.PCP.Hastad.hastadLinearProb_longCode {β : Type u_2} {γ : Type u_3} [Fintype β] [DecidableEq β] [Fintype γ] [DecidableEq γ] (π : β → γ) (δ : ℝ) (x : β) :
      hastadLinearProb π δ (BitString.longCode (π x)) (BitString.longCode x) = 1 - δ

      Completeness of Håstad's 3-bit linear test (probability): matching Long Code tables longCode (π x) and longCode x pass the test with probability 1 - δ.

      source
      theorem Cslib.PCP.Hastad.hastadLinearCorr_eq_sum {β : Type u_2} {γ : Type u_3} [Fintype β] [DecidableEq β] [Fintype γ] [DecidableEq γ] (π : β → γ) (δ : ℝ) (B : (γ → Bool) → Bool) (A : (β → Bool) → Bool) :
      hastadLinearCorr π δ B A = ∑ T : Finset β, (1 - 2 * δ) ^ T.card * BitString.fourierCoeff (fun (g : β → Bool) => BitString.signVal (A g)) T ^ 2 * BitString.fourierCoeff (fun (f : γ → Bool) => BitString.signVal (B f)) (BitString.projectSet π T)

      Walsh–Fourier expansion of Håstad's 3-bit linear test Håstad, Lemma 5.1: the correlation equals ∑ T : Finset β, (1 - 2 * δ) ^ #T * fourierCoeff F_A T ^ 2 * fourierCoeff F_B (projectSet π T).

      Spectral decoding weights and Cauchy–Schwarz soundness bound #

      source
      noncomputable def Cslib.PCP.Hastad.spectralWeight {α : Type u_1} [Fintype α] [DecidableEq α] (k : ℕ) (A : (α → Bool) → Bool) (x : α) :
      ℝ

      The low-degree spectral decoding weight of x : α for table A : (α → Bool) → Bool at degree cutoff k: ∑_{T : #T < k, x ∈ T} fourierCoeff F_A T ^ 2 / #T Håstad, Proof of Lemma 5.2.

      Instances For
        source
        theorem Cslib.PCP.Hastad.spectralWeight_nonneg {α : Type u_1} [Fintype α] [DecidableEq α] (k : ℕ) (A : (α → Bool) → Bool) (x : α) :
        0 ≤ spectralWeight k A x
        source
        theorem Cslib.PCP.Hastad.sum_spectralWeight_le_one {α : Type u_1} [Fintype α] [DecidableEq α] (k : ℕ) (A : (α → Bool) → Bool) :
        ∑ x : α, spectralWeight k A x ≤ 1

        By Parseval's identity, the spectral decoding weights form a sub-probability distribution: ∑ x, spectralWeight k A x ≤ 1.

        source
        theorem Cslib.PCP.Hastad.hastadLinearCorr_sq_le {β : Type u_2} {γ : Type u_3} [Fintype β] [DecidableEq β] [Fintype γ] [DecidableEq γ] (π : β → γ) {δ : ℝ} (hδ0 : 0 ≤ δ) (hδ1 : δ ≤ 1 / 2) (k : ℕ) {B : (γ → Bool) → Bool} (hB : BitString.IsOdd B) (A : (β → Bool) → Bool) :
        hastadLinearCorr π δ B A ^ 2 ≤ (1 - 2 * δ) ^ (2 * k) + ↑k ^ 2 * ∑ x : β, spectralWeight k A x * spectralWeight k B (π x)

        Cauchy–Schwarz and Parseval soundness bound for Håstad's 3-bit linear test Håstad, Lemma 5.2: for any folded (odd) table B, any table A, noise rate 0 ≤ δ ≤ 1 / 2, and degree cutoff k, the squared correlation hastadLinearCorr π δ B A ^ 2 is at most (1 - 2 * δ) ^ (2 * k) + k ^ 2 * ∑ x, spectralWeight k A x * spectralWeight k B (π x).