The Hadamard code

The Hadamard code (or Walsh–Hadamard code) encodes a bit string x : ι → Bool as the truth table of the function a ↦ x ⬝ᵥ a, the dot product in the Boolean ring Bool, that is, the inner product modulo two (BitString.hadamardCode). Bit strings add coordinatewise through the same ring structure, and the code is bilinear (BitString.hadamardCode_add, BitString.hadamardCode_add_left). Its codewords are exactly the parities, hence exactly the linear Boolean functions (BitString.exists_eq_hadamardCode_iff). Two distinct codewords of n bits differ on half of the 2 ^ n inputs (BitString.two_mul_hammingDist_hadamardCode), so for n ≥ 1 the Hadamard code has minimum distance 2 ^ (n - 1) (BitString.minDist_range_hadamardCode).

A function f that is close to a parity can be self-corrected: to read the parity at x, read f at a uniformly random y and at x + y, both uniformly distributed, and add the two bits (BitString.selfCorrect). If f differs from the parity on an ε fraction of the inputs, this returns the parity's value at x with probability at least 1 - 2ε, whatever x is (BitString.one_sub_two_mul_le_expect_selfCorrect). For the Hadamard code this is a two-query local decoder: the i-th bit of the message is read off at the i-th unit vector (BitString.one_sub_two_mul_le_expect_selfCorrect_eq_apply). A word within relative distance δ < 1/4 of a codeword determines the codeword (BitString.eq_of_hammingDist_hadamardCode_le) O'Donnell, Section 1.6, Arora and Barak, Chapters 11 and 19.

Main definitions

• Cslib.BitString.selfCorrect: the two-query self-corrected read of a Boolean function.
• Cslib.BitString.hadamardCode: the Hadamard encoding of a bit string.

Main results

• Cslib.BitString.hadamardCode_eq_parityOn: a codeword is a parity.
• Cslib.BitString.card_filter_selfCorrect_ne_le, Cslib.BitString.one_sub_two_mul_le_expect_selfCorrect: local correctability of parities.
• Cslib.BitString.exists_eq_hadamardCode_iff: the codewords are the linear functions.
• Cslib.BitString.hadamardCode_injective, Cslib.BitString.two_mul_hammingDist_hadamardCode, Cslib.BitString.minDist_range_hadamardCode: the Hadamard code is injective with relative distance one half and minimum distance 2 ^ (n - 1).
• Cslib.BitString.eq_of_hammingDist_hadamardCode_le: unique decoding below distance 1/4.
• Cslib.BitString.one_sub_two_mul_le_expect_selfCorrect_eq_apply: local decoding with two queries.

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

Self-correction

def Cslib.BitString.selfCorrect {ι : Type u_1} (f : (ι → Bool) → Bool) (x y : ι → Bool) : Bool

The self-corrected read of f at x with randomness y: the exclusive or of f y and f (x + y). For uniformly random y, both points read are uniformly random, and on a parity the read is exact (selfCorrect_parityOn).

@[simp]

theorem Cslib.BitString.selfCorrect_parityOn {ι : Type u_1} (S : Finset ι) (x y : ι → Bool) : selfCorrect (parityOn S) x y = parityOn S x

Self-correction reads a parity exactly.

theorem Cslib.BitString.card_filter_selfCorrect_ne_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) (S : Finset ι) (x : ι → Bool) : {y : ι → Bool | selfCorrect f x y ≠ parityOn S x}.card ≤ 2 * hammingDist f (parityOn S)

Local correctability of parities, counting version: the self-corrected read of f at x differs from the parity on S at x for at most twice as many y as there are inputs on which f differs from that parity.

theorem Cslib.BitString.one_sub_two_mul_le_expect_selfCorrect {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → Bool} {S : Finset ι} {ε : ℝ} (h : ↑(hammingDist f (parityOn S)) / 2 ^ Fintype.card ι ≤ ε) (x : ι → Bool) : 1 - 2 * ε ≤ Finset.univ.expect fun (y : ι → Bool) => if selfCorrect f x y = parityOn S x then 1 else 0

Local correctability of parities: if f differs from the parity on S on at most an ε fraction of the inputs, then for every x, self-correction at x returns the parity's value at x with probability at least 1 - 2ε over a uniformly random y O'Donnell, Proposition 1.31.

The Hadamard code

def Cslib.BitString.hadamardCode {ι : Type u_1} [Fintype ι] (x : ι → Bool) : (ι → Bool) → Bool

The Hadamard encoding of x: the Boolean function sending a to the dot product x ⬝ᵥ a in the Boolean ring Bool, the inner product of x and a modulo two Arora and Barak, Section 11.5.

@[simp]

theorem Cslib.BitString.hadamardCode_apply {ι : Type u_1} [Fintype ι] (x a : ι → Bool) : hadamardCode x a = x ⬝ᵥ a

The Hadamard codeword of x at a is the dot product x ⬝ᵥ a.

theorem Cslib.BitString.hadamardCode_eq_parityOn {ι : Type u_1} [Fintype ι] (x : ι → Bool) : hadamardCode x = parityOn {i : ι | x i = true}

A Hadamard codeword is the parity of the bits at the positions where the message is true.

theorem Cslib.BitString.hadamardCode_comm {ι : Type u_1} [Fintype ι] (x a : ι → Bool) : hadamardCode x a = hadamardCode a x

The inner product is symmetric.

theorem Cslib.BitString.hadamardCode_add {ι : Type u_1} [Fintype ι] (x a b : ι → Bool) : hadamardCode x (a + b) = (hadamardCode x a ^^ hadamardCode x b)

Hadamard codewords are linear.

theorem Cslib.BitString.hadamardCode_add_left {ι : Type u_1} [Fintype ι] (x y a : ι → Bool) : hadamardCode (x + y) a = (hadamardCode x a ^^ hadamardCode y a)

The Hadamard code is linear.

@[simp]

theorem Cslib.BitString.selfCorrect_hadamardCode {ι : Type u_1} [Fintype ι] (x a y : ι → Bool) : selfCorrect (hadamardCode x) a y = hadamardCode x a

Self-correction reads a Hadamard codeword exactly.

theorem Cslib.BitString.hadamardCode_decide_mem {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : Finset ι) : (hadamardCode fun (i : ι) => decide (i ∈ S)) = parityOn S

The parity on S is the Hadamard encoding of the indicator of S.

@[simp]

theorem Cslib.BitString.hadamardCode_single {ι : Type u_1} [Fintype ι] [DecidableEq ι] (x : ι → Bool) (i : ι) : hadamardCode x (Pi.single i true) = x i

The value of a Hadamard codeword at the i-th unit vector is the i-th bit of the message.

theorem Cslib.BitString.exists_eq_hadamardCode_iff {ι : Type u_1} [Fintype ι] {f : (ι → Bool) → Bool} : (∃ (x : ι → Bool), f = hadamardCode x) ↔ ∀ (x y : ι → Bool), f (x + y) = (f x ^^ f y)

The Hadamard codewords are the linear Boolean functions.

theorem Cslib.BitString.hadamardCode_injective {ι : Type u_1} [Fintype ι] : Function.Injective hadamardCode

The Hadamard code is injective.

theorem Cslib.BitString.two_mul_hammingDist_hadamardCode {ι : Type u_1} [Fintype ι] [DecidableEq ι] {x y : ι → Bool} (h : x ≠ y) : 2 * hammingDist (hadamardCode x) (hadamardCode y) = 2 ^ Fintype.card ι

The Hadamard code has relative distance one half: the encodings of distinct bit strings differ on exactly half of the inputs.

theorem Cslib.BitString.eq_of_hammingDist_hadamardCode_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → Bool} {x y : ι → Bool} {δ : ℝ} (hδ : δ < 1 / 4) (hx : ↑(hammingDist f (hadamardCode x)) / 2 ^ Fintype.card ι ≤ δ) (hy : ↑(hammingDist f (hadamardCode y)) / 2 ^ Fintype.card ι ≤ δ) : x = y

Unique decoding: a Boolean function within relative distance δ < 1/4 of the encodings of x and of y forces x = y.

theorem Cslib.BitString.one_sub_two_mul_le_expect_selfCorrect_hadamardCode {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → Bool} {x : ι → Bool} {ε : ℝ} (h : ↑(hammingDist f (hadamardCode x)) / 2 ^ Fintype.card ι ≤ ε) (a : ι → Bool) : 1 - 2 * ε ≤ Finset.univ.expect fun (y : ι → Bool) => if selfCorrect f a y = hadamardCode x a then 1 else 0

Local correction for the Hadamard code: if f is within relative distance ε of the encoding of x, then for every a, self-correction at a returns the codeword's value at a with probability at least 1 - 2ε.

theorem Cslib.BitString.one_sub_two_mul_le_expect_selfCorrect_eq_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → Bool} {x : ι → Bool} {ε : ℝ} (h : ↑(hammingDist f (hadamardCode x)) / 2 ^ Fintype.card ι ≤ ε) (i : ι) : 1 - 2 * ε ≤ Finset.univ.expect fun (y : ι → Bool) => if selfCorrect f (Pi.single i true) y = x i then 1 else 0

Local decoding of the Hadamard code with two queries: if f is within relative distance ε of the encoding of x, then self-correction at the i-th unit vector returns x i with probability at least 1 - 2ε Arora and Barak, Section 11.5.

theorem Cslib.BitString.minDist_range_hadamardCode {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] : Code.minDist (Set.range hadamardCode) = ↑(2 ^ (Fintype.card ι - 1))

The distance of the Hadamard code. For messages of n ≥ 1 bits, the Hadamard code has minimum distance 2 ^ (n - 1): half of its length 2 ^ n.