Decoding the Hadamard code from the BLR linearity test

Hadamard codewords (BitString.hadamardCode) are parities, so they pass the Blum–Luby–Rubinfeld linearity test with probability one (BitString.blrAcceptance_hadamardCode). Conversely, by the Fourier soundness of the test (BitString.exists_hammingDist_parityOn_le_of_le_blrAcceptance), a Boolean function that passes the test with probability at least 1 - ε is within relative Hamming distance ε of the Hadamard encoding of some message (BitString.exists_hammingDist_hadamardCode_le_of_le_blrAcceptance), and when ε < 1/4 that message is unique (BitString.existsUnique_hammingDist_hadamardCode_le_of_le_blrAcceptance) O'Donnell, Section 1.6, Arora and Barak, Section 11.5.

Main results

• Cslib.BitString.blrAcceptance_hadamardCode: Hadamard codewords pass the BLR test with probability one.
• Cslib.BitString.exists_hammingDist_hadamardCode_le_of_le_blrAcceptance, Cslib.BitString.existsUnique_hammingDist_hadamardCode_le_of_le_blrAcceptance: decoding a function that passes the linearity test.

References

• M. Blum, M. Luby, R. Rubinfeld, Self-testing/correcting with applications to numerical problems
• R. O'Donnell, Analysis of Boolean Functions
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

@[simp]

theorem Cslib.BitString.blrAcceptance_hadamardCode {ι : Type u_1} [Fintype ι] [DecidableEq ι] (x : ι → Bool) : blrAcceptance (hadamardCode x) = 1

Hadamard codewords pass the BLR test with probability one.

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

Decoding from the BLR test: if the test accepts f with probability at least 1 - ε, then f is within relative distance ε of the Hadamard encoding of some bit string.

theorem Cslib.BitString.existsUnique_hammingDist_hadamardCode_le_of_le_blrAcceptance {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → Bool} {ε : ℝ} (hε : ε < 1 / 4) (h : 1 - ε ≤ blrAcceptance f) : ∃! x : ι → Bool, ↑(hammingDist f (hadamardCode x)) / 2 ^ Fintype.card ι ≤ ε

Unique decoding from the BLR test: if the test accepts f with probability at least 1 - ε and ε < 1/4, then exactly one bit string has its Hadamard encoding within relative distance ε of f.