The long code, odd Boolean functions, folding, and projections of characters

The long code of a label a : ι is the dictator r ↦ r a, the evaluation Function.eval a on ι → Bool (BitString.longCode) Arora and Barak, Chapter 22. It is the Hadamard encoding of the unit vector of a (BitString.longCode_eq_hadamardCode), so a table within relative distance 1/4 of a long code determines its label (BitString.eq_of_hammingDist_longCode_lt).

A Boolean function B : (ι → Bool) → Bool is odd (BitString.IsOdd) when complementing its input complements its output, B (f + 1) = !B f; in ±1 notation this is F (-x) = -F x, and such functions are also called self-dual. In PCP constructions, odd long code tables are called folded. Every long code is odd (BitString.isOdd_longCode), every table can be folded around a coordinate into an odd one (BitString.foldTable), and the Fourier coefficients of an odd function vanish on every set of even cardinality (BitString.IsOdd.fourierCoeff_of_even), in particular on ∅ (BitString.IsOdd.fourierCoeff_empty).

For a map π : β → γ, the mod-2 projection BitString.projectSet π T of T : Finset β is the set of points of γ with an odd number of preimages in T. Pulling a character back along π projects its frequency set: chi T (f ∘ π) = chi (projectSet π T) f (BitString.chi_comp_eq_chi_projectSet) Håstad, O'Donnell, Chapter 7.

Main definitions

• Cslib.BitString.longCode: the long code of a label.
• Cslib.BitString.IsOdd: odd (folded) Boolean functions.
• Cslib.BitString.foldTable: folding a table around a coordinate.
• Cslib.BitString.projectSet: the mod-2 projection of a set along a map.

Main results

• Cslib.BitString.longCode_eq_hadamardCode, Cslib.BitString.eq_of_hammingDist_longCode_lt: the long code is a Hadamard code, and unique decoding of the long code.
• Cslib.BitString.isOdd_longCode, Cslib.BitString.isOdd_foldTable: long codes and folded tables are odd.
• Cslib.BitString.IsOdd.fourierCoeff_empty, Cslib.BitString.IsOdd.fourierCoeff_of_even: odd functions have no Fourier weight on sets of even cardinality.
• Cslib.BitString.chi_comp_eq_chi_projectSet: pulling a character back along a map.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• J. Håstad, Some optimal inapproximability results
• R. O'Donnell, Analysis of Boolean Functions

The long code

def Cslib.BitString.longCode {ι : Type u_1} (a : ι) : (ι → Bool) → Bool

The long code of a label a : ι: the dictator r ↦ r a on ι → Bool, that is, the evaluation Function.eval a Arora and Barak, Chapter 22. It is the Hadamard encoding of the unit vector of a (longCode_eq_hadamardCode).

@[simp]

theorem Cslib.BitString.longCode_apply {ι : Type u_1} (a : ι) (r : ι → Bool) : longCode a r = r a

The long code of a reads the bit of r at a.

theorem Cslib.BitString.longCode_eq_hadamardCode {ι : Type u_1} [Fintype ι] [DecidableEq ι] (a : ι) : longCode a = hadamardCode (Pi.single a true)

The long code of a is the Hadamard encoding of the unit vector of a.

theorem Cslib.BitString.eq_of_hammingDist_longCode_lt {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → Bool} {a b : ι} (ha : ↑(hammingDist f (longCode a)) / 2 ^ Fintype.card ι < 1 / 4) (hb : ↑(hammingDist f (longCode b)) / 2 ^ Fintype.card ι < 1 / 4) : a = b

Unique decoding of the long code: a Boolean function within relative distance less than 1/4 of the long codes of a and of b forces a = b.

Odd functions and folding

theorem Cslib.BitString.signVal_longCode {α : Type u_2} (x : α) (f : α → Bool) : signVal (longCode x f) = chi ℝ {x} f

In ±1 notation, the long code longCode x is the singleton character chi ℝ {x}.

def Cslib.BitString.IsOdd {α : Type u_2} (B : (α → Bool) → Bool) : Prop

A Boolean function B : (α → Bool) → Bool is odd when complementing the input (f + fun _ => true) complements the output. In ±1 notation this says F (-x) = -F x; such functions are also called self-dual, and odd long code tables are called folded.

theorem Cslib.BitString.isOdd_longCode {α : Type u_2} (x : α) : IsOdd (longCode x)

Every long code longCode x is odd.

def Cslib.BitString.foldTable {α : Type u_2} (x₀ : α) (B : (α → Bool) → Bool) (f : α → Bool) : Bool

Folding a table around the coordinate x₀ : α: it reads B f when f x₀ = false and !B (f + fun _ => true) when f x₀ = true.

theorem Cslib.BitString.isOdd_foldTable {α : Type u_2} (x₀ : α) (B : (α → Bool) → Bool) : IsOdd (foldTable x₀ B)

Folding any table produces an odd table.

theorem Cslib.BitString.IsOdd.foldTable_eq {α : Type u_2} {B : (α → Bool) → Bool} (hB : IsOdd B) (x₀ : α) : foldTable x₀ B = B

Folding an odd table leaves it unchanged.

theorem Cslib.BitString.IsOdd.fourierCoeff_empty {α : Type u_2} [Fintype α] [DecidableEq α] {B : (α → Bool) → Bool} (hB : IsOdd B) : fourierCoeff (fun (f : α → Bool) => signVal (B f)) ∅ = 0

An odd function has zero empty Fourier coefficient: its ±1 values at f and f + fun _ => true cancel.

theorem Cslib.BitString.IsOdd.fourierCoeff_of_even {α : Type u_2} [Fintype α] [DecidableEq α] {B : (α → Bool) → Bool} (hB : IsOdd B) {S : Finset α} (hS : Even S.card) : fourierCoeff (fun (f : α → Bool) => signVal (B f)) S = 0

An odd function has Fourier coefficient 0 on every set of even cardinality.

Mod-2 projection of subsets and character pullback

def Cslib.BitString.projectSet {β : Type u_3} {γ : Type u_4} [Fintype γ] [DecidableEq γ] (π : β → γ) (T : Finset β) : Finset γ

The mod-2 projection π₂(T) of T : Finset β along π : β → γ: the set of y : γ whose fiber in T under π has odd cardinality Håstad.

@[simp]

theorem Cslib.BitString.mem_projectSet {β : Type u_3} {γ : Type u_4} [Fintype γ] [DecidableEq γ] {π : β → γ} {T : Finset β} {y : γ} : y ∈ projectSet π T ↔ Odd {x ∈ T | π x = y}.card

y lies in the mod-2 projection of T exactly when its fiber in T has odd cardinality.

@[simp]

theorem Cslib.BitString.projectSet_empty {β : Type u_3} {γ : Type u_4} [Fintype γ] [DecidableEq γ] (π : β → γ) : projectSet π ∅ = ∅

The mod-2 projection of the empty set is empty.

theorem Cslib.BitString.exists_mem_of_mem_projectSet {β : Type u_3} {γ : Type u_4} [Fintype γ] [DecidableEq γ] {π : β → γ} {T : Finset β} {y : γ} (hy : y ∈ projectSet π T) : ∃ x ∈ T, π x = y

Every element of projectSet π T lies in the image of T under π.

theorem Cslib.BitString.projectSet_subset_image {β : Type u_3} {γ : Type u_4} [Fintype γ] [DecidableEq γ] (π : β → γ) (T : Finset β) : projectSet π T ⊆ Finset.image π T

The mod-2 projection of T along π is contained in the image T.image π.

theorem Cslib.BitString.card_projectSet_le {β : Type u_3} {γ : Type u_4} [Fintype γ] [DecidableEq γ] (π : β → γ) (T : Finset β) : (projectSet π T).card ≤ T.card

The mod-2 projection never increases cardinality: #(projectSet π T) ≤ #T.

theorem Cslib.BitString.projectSet_insert {β : Type u_3} {γ : Type u_4} [Fintype γ] [DecidableEq γ] [DecidableEq β] (π : β → γ) {x : β} {T : Finset β} (hx : x ∉ T) : projectSet π (insert x T) = symmDiff (projectSet π T) {π x}

Inserting x ∉ T toggles π x in projectSet π T.

theorem Cslib.BitString.chi_comp_eq_chi_projectSet {β : Type u_3} {γ : Type u_4} [Fintype γ] [DecidableEq γ] (π : β → γ) (T : Finset β) (f : γ → Bool) : chi ℝ T (f ∘ π) = chi ℝ (projectSet π T) f

Pulling a character back along π projects the frequency set by projectSet π: chi ℝ T (f ∘ π) = chi ℝ (projectSet π T) f.