Majority votes

If at least two thirds of the elements of a finite type Ω are good, then among the tuples of 2 r elements of Ω, those in which at most half of the entries are good make up at most an (8 / 9) ^ r fraction. This is the error bound for repeating a bounded-error test 2 r times independently and taking the majority answer, in counting form.

The proof is the exponential-moment (Chernoff) argument with weight 2 on the bad elements: the weights of all tuples sum to (|good| + 2 |bad|) ^ (2 r) ≤ (4 |Ω| / 3) ^ (2 r), and a tuple with at most r good entries has weight at least 2 ^ r.

Main results

• Cslib.card_filter_card_filter_le_le: the bound.
• Cslib.exists_forall_lt_card_filter_mem: for a family of at most 2 ^ n tests, each passed by two thirds of Ω, some 12 (n + 1) elements of Ω contain a majority passing each test.
• Cslib.exists_forall_exists_apply_mem: for a family of at most 2 ^ n tests, each passed by half of Ω, some n + 1 elements of Ω contain one passing each test; this is the exact finite-cover union bound with failure ratio 1 / 2.
• Cslib.two_pow_mul_eight_pow_lt: the numeric bound 2 ^ n * 8 ^ (6 n + 6) < 9 ^ (6 n + 6) behind the choice of 12 (n + 1) repetitions.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 7.4

theorem Cslib.card_filter_card_filter_le_le {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (G : Finset Ω) (hG : 2 * Fintype.card Ω ≤ 3 * G.card) (r : ℕ) : 9 ^ r * {ω : Fin (2 * r) → Ω | {i : Fin (2 * r) | ω i ∈ G}.card ≤ r}.card ≤ 8 ^ r * Fintype.card Ω ^ (2 * r)

Majority votes. If at least two thirds of Ω lie in G, then at most an (8 / 9) ^ r fraction of the 2 r-tuples have at most r entries in G.

theorem Cslib.two_pow_mul_eight_pow_lt (n : ℕ) : 2 ^ n * 8 ^ (6 * n + 6) < 9 ^ (6 * n + 6)

For any n, 2 ^ n * 8 ^ (6 * n + 6) < 9 ^ (6 * n + 6), since 2 * 8 ^ 6 < 9 ^ 6.

theorem Cslib.exists_forall_lt_card_filter_mem {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {X : Type u_2} [Fintype X] [Nonempty Ω] {n : ℕ} (hX : Fintype.card X ≤ 2 ^ n) (good : X → Finset Ω) (hgood : ∀ (x : X), 2 * Fintype.card Ω ≤ 3 * (good x).card) : ∃ (ω : Fin (2 * (6 * n + 6)) → Ω), ∀ (x : X), 6 * n + 6 < {i : Fin (2 * (6 * n + 6)) | ω i ∈ good x}.card

Majority votes good for many tests at once. If each of at most 2 ^ n tests is passed by at least two thirds of Ω, then some 12 (n + 1) elements of Ω contain more than 6 (n + 1) elements passing each test.

theorem Cslib.exists_forall_exists_apply_mem {Ω : Type u_1} [Fintype Ω] {X : Type u_2} [Fintype X] [Nonempty Ω] {n : ℕ} (hX : Fintype.card X ≤ 2 ^ n) (good : X → Finset Ω) (hgood : ∀ (x : X), Fintype.card Ω ≤ 2 * (good x).card) : ∃ (ω : Fin (n + 1) → Ω), ∀ (x : X), ∃ (i : Fin (n + 1)), ω i ∈ good x

One good element for many tests at once. If each of at most 2 ^ n tests is passed by at least half of Ω, then some n + 1 elements of Ω contain one passing each test.