Documentation

Complexity.Foundations.BooleanAnalysis.Linearity

Linearity testing #

A Boolean function on the cube is linear when it turns sums into sums, f (x + y) = (f x ^^ f y), where bit strings add coordinatewise modulo two (x + y, through Mathlib's Boolean ring structure on Bool) and single bits by exclusive or (^^). The linear functions are exactly the parities (BitString.exists_eq_parityOn_iff, with parityOn_add). Distinct parities differ on half of the inputs (BitString.two_mul_hammingDist_parityOn, from Complexity.Foundations.Data.BitString.Hamming), and a linear function that is not constantly false takes the value true on half of the inputs (BitString.expect_boole_eq_one_div_two_of_map_add).

The Blum–Luby–Rubinfeld test queries f at independent uniformly random x and y and at x + y, and accepts when (f x ^^ f y) = f (x + y); BitString.blrAcceptance f is the probability that it accepts. Reading f as the function F x = (-1) ^ f x, the test accepts with probability 1/2 + 1/2 ∑_S F̂(S)³ (BitString.blrAcceptance_eq_sum_fourierCoeff_pow_three), by the convolution theorem. Parities pass with probability one (BitString.blrAcceptance_parityOn). Conversely, a function passing with probability at least 1 - ε differs from some parity on at most an ε fraction of the inputs (BitString.exists_hammingDist_parityOn_le_of_le_blrAcceptance): the squares F̂(S)² sum to one by Parseval's identity, so ∑_S F̂(S)³ ≤ max_S F̂(S), and F̂(S) is one minus twice the relative Hamming distance from f to the parity on S (BitString.fourierCoeff_signVal) O'Donnell, Section 1.6, [BLR93].

Main definitions #

Main results #

References #

Linear functions #

source
theorem Cslib.BitString.expect_boole_eq_one_div_two_of_map_add {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → Bool} (hf : ∀ (x y : ι → Bool), f (x + y) = (f x ^^ f y)) (h : ∃ (x : ι → Bool), f x = true) :
(Finset.univ.expect fun (x : ι → Bool) => if f x = true then 1 else 0) = 1 / 2

Nonzero linear functions are balanced: a Boolean function that turns sums of bit strings into the exclusive or of its values, and is not constantly false, takes the value true with probability one half at a uniformly random input.

The Blum–Luby–Rubinfeld test #

source
noncomputable def Cslib.BitString.blrAcceptance {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) :
ℝ

The acceptance probability of the Blum–Luby–Rubinfeld linearity test on f: the probability, over independent uniformly random bit strings x and y, that (f x ^^ f y) = f (x + y).

Instances For
    source
    theorem Cslib.BitString.blrAcceptance_eq_sum_fourierCoeff_pow_three {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) :
    blrAcceptance f = 1 / 2 + 1 / 2 * ∑ S : Finset ι, fourierCoeff (fun (x : ι → Bool) => signVal (f x)) S ^ 3

    The acceptance probability of the BLR test: reading f as signs, the test accepts with probability 1/2 + 1/2 ∑_S F̂(S)³.

    source
    theorem Cslib.BitString.blrAcceptance_parityOn {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : Finset ι) :
    blrAcceptance (parityOn S) = 1

    Completeness of the BLR test: parities pass with probability one.

    source
    theorem Cslib.BitString.exists_hammingDist_parityOn_le_of_le_blrAcceptance {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → Bool} {ε : ℝ} (h : 1 - ε ≤ blrAcceptance f) :
    ∃ (S : Finset ι), ↑(hammingDist f (parityOn S)) / 2 ^ Fintype.card ι ≤ ε

    Soundness of the BLR test: if the test accepts f with probability at least 1 - ε, then f differs from some parity on at most an ε fraction of the inputs O'Donnell, Theorem 1.30.