Lautemann's covering lemma

The combinatorial core of the Sipser–Lautemann theorem, stated for an event E in the seed space Fin m → Bool and the XOR shift action on that space.

def Complexity.Lautemann.shift {m : ℕ} (r u : Fin m → Bool) : Fin m → Bool

XOR shift of a seed by a vector.

Equations

• Complexity.Lautemann.shift r u i = (r i ^^ u i)

@[simp]

theorem Complexity.Lautemann.shift_shift {m : ℕ} (r u : Fin m → Bool) : shift (shift r u) u = r

theorem Complexity.Lautemann.shift_comm {m : ℕ} (r u : Fin m → Bool) : shift r u = shift u r

The shift action is symmetric in its two arguments.

def Complexity.Lautemann.shiftEquiv {m : ℕ} (u : Fin m → Bool) : (Fin m → Bool) ≃ (Fin m → Bool)

Shifting by a fixed vector is an involutive equivalence of the seed space.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.Lautemann.Covers {m t : ℕ} (E : Finset (Fin m → Bool)) (u : Fin t → Fin m → Bool) : Prop

The t shifts u 0, …, u (t-1) of the event E cover the whole seed space: every seed lands in E after at least one of them.

Equations

• Complexity.Lautemann.Covers E u = ∀ (r : Fin m → Bool), ∃ (i : Fin t), Complexity.Lautemann.shift r (u i) ∈ E

theorem Complexity.Lautemann.card_filter_shift_mem {m : ℕ} (E : Finset (Fin m → Bool)) (u : Fin m → Bool) : {r : Fin m → Bool | shift r u ∈ E}.card = E.card

Shifting is measure preserving: the seeds carried into E by a fixed shift are as many as the elements of E.

theorem Complexity.Lautemann.card_univ_seed {m : ℕ} : Finset.univ.card = 2 ^ m

The number of seeds is 2 ^ m.

theorem Complexity.Lautemann.card_univ_shifts {m t : ℕ} : Finset.univ.card = (2 ^ m) ^ t

The number of t-tuples of shift vectors is (2 ^ m) ^ t.

theorem Complexity.Lautemann.exists_covers_of_card {m t : ℕ} (E : Finset (Fin m → Bool)) (h : 2 ^ m * (2 ^ m - E.card) ^ t < (2 ^ m) ^ t) : ∃ (u : Fin t → Fin m → Bool), Covers E u

Existence of covering shifts. If the complement of E is small enough that 2 ^ m translates of its m-fold product miss the whole shift space, some m-tuple of shifts covers every seed. This is the counting form of the probabilistic argument: a uniformly random tuple fails to cover a fixed seed with probability (1 - eventProb E) ^ m, and a union bound over the 2 ^ m seeds leaves a covering tuple.

theorem Complexity.Lautemann.not_covers_of_card {m t : ℕ} (E : Finset (Fin m → Bool)) (h : t * E.card < 2 ^ m) (u : Fin t → Fin m → Bool) : ¬Covers E u

No covering when the event is small. If t copies of E cannot fill the seed space by cardinality alone, no tuple of t shifts covers it.

Probability form

theorem Complexity.Lautemann.card_mul_two_pow_le {m k : ℕ} (E : Finset (Fin m → Bool)) (h : eventProb E ≤ 1 / 2 ^ k) : E.card * 2 ^ k ≤ 2 ^ m

An event of probability at most 2 ^ (-k) has at most 2 ^ (m - k) elements, in the multiplication-only form used below.

theorem Complexity.Lautemann.exists_covers_of_eventProb_compl_le {m t k : ℕ} (E : Finset (Fin m → Bool)) (hmt : m < k * t) (h : eventProb Eᶜ ≤ 1 / 2 ^ k) : ∃ (u : Fin t → Fin m → Bool), Covers E u

Lautemann's covering lemma, completeness direction. If the event E fails with probability at most 2 ^ (-k), and the seed length m is below k * t, then some t shifts of E cover the whole seed space. Since the failure probability enters as its t-th power against a union bound over the 2 ^ m seeds, any k ≥ 2 suffices at t ≥ m.

theorem Complexity.Lautemann.not_covers_of_eventProb_le {m t k : ℕ} (E : Finset (Fin m → Bool)) (hk : t < 2 ^ k) (h : eventProb E ≤ 1 / 2 ^ k) (u : Fin t → Fin m → Bool) : ¬Covers E u

Lautemann's covering lemma, soundness direction. If the event E holds with probability at most 2 ^ (-k) and the number of shifts t is below 2 ^ k, then no t shifts of E cover the seed space.