Ternary majority trees and counting amplification

A majority tree (Cslib.majTree) of depth L combines 3 ^ L outcomes by repeated majorities of three, maj3 a b c = if a = b then a else c, which is right whenever two of its arguments are. If a single outcome errs on at most a ρ fraction of a finite sample space, the tree errs on at most a (3 * ρ) ^ (2 ^ L) / 3 fraction of the 3 ^ L-tuples (Cslib.card_majTree_ne_le). For 3 * ρ ≤ 1 / 2 this is below 2 ^ (-2 ^ L), so by a union bound one fixed choice of the 3 ^ L outcomes is right on every element of a set of at most 2 ^ (2 ^ L) targets (Cslib.exists_forall_majTree_eq). Majority trees replace a Chernoff bound by a counting argument and need only equality tests to evaluate Arora and Barak, Chapter 19.

Main definitions

• Cslib.maj3, Cslib.majTree: majorities of three and majority trees.
• Cslib.tripleEquiv: the splitting of 3 ^ (L + 1) indices into three blocks of 3 ^ L.

Main results

• Cslib.card_majTree_ne_le: amplification by majority trees.
• Cslib.exists_forall_majTree_eq: one choice of outcomes is right across a whole set.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Chapter 19

def Cslib.maj3 {α : Type u_1} [DecidableEq α] (a b c : α) : α

The majority of three, right whenever two of its arguments are: a if a = b, else c.

theorem Cslib.two_ne_of_maj3_ne {α : Type u_1} [DecidableEq α] {a b c y : α} (h : maj3 a b c ≠ y) : a ≠ y ∧ b ≠ y ∨ a ≠ y ∧ c ≠ y ∨ b ≠ y ∧ c ≠ y

If maj3 a b c misses y, then two of a, b, c miss y.

def Cslib.tripleEquiv (L : ℕ) : Fin 3 × Fin (3 ^ L) ≃ Fin (3 ^ (L + 1))

The splitting of 3 ^ (L + 1) leaves into three blocks of 3 ^ L.

def Cslib.majTree {α : Type u_1} [DecidableEq α] (L : ℕ) : (Fin (3 ^ L) → α) → α

A majority tree of depth L over 3 ^ L values: the majority of three of the trees over the three blocks.

theorem Cslib.card_majTree_ne_le {α : Type u_1} [DecidableEq α] {Ω : Type u_2} [Fintype Ω] (val : Ω → α) (y : α) {ρ : ℝ} (hρ : ↑{ω : Ω | val ω ≠ y}.card ≤ ρ * ↑(Fintype.card Ω)) (L : ℕ) : ↑{V : Fin (3 ^ L) → Ω | majTree L (val ∘ V) ≠ y}.card ≤ (3 * ρ) ^ 2 ^ L / 3 * ↑(Fintype.card Ω) ^ 3 ^ L

Amplification by majority trees. If at most a ρ fraction of the outcomes ω have val ω ≠ y, then at most a (3 * ρ) ^ (2 ^ L) / 3 fraction of the tuples of 3 ^ L outcomes make the majority tree miss y.

theorem Cslib.exists_forall_majTree_eq {α : Type u_1} [DecidableEq α] {X : Type u_2} {Ω : Type u_3} [Fintype Ω] [Nonempty Ω] (S : Finset X) (val : X → Ω → α) (target : X → α) {ρ : ℝ} (hρ : ∀ x ∈ S, ↑{ω : Ω | val x ω ≠ target x}.card ≤ ρ * ↑(Fintype.card Ω)) (h3 : 3 * ρ ≤ 1 / 2) {L : ℕ} (hS : S.card ≤ 2 ^ 2 ^ L) : ∃ (V : Fin (3 ^ L) → Ω), ∀ x ∈ S, majTree L (val x ∘ V) = target x

One choice of randomness corrects a whole set. Let a randomized procedure val x, for each x in a set S of at most 2 ^ (2 ^ L) inputs, miss target x on at most a ρ fraction of its outcomes, with 3 * ρ ≤ 1 / 2. Then some tuple of 3 ^ L outcomes makes the majority tree right at every x ∈ S.