Korten's strong mirror-set lemma

A point x is a (p, k)-limit of a set Y of points of the cube (IsDensityLimit, Korten, Definition 2) when, with probability at least 3 / 4 over a random mask P of rate p, the fiber of Y over the coordinates of x outside P has density at least 2 ^ (-k). If every point of a nonempty set X of deficit at most k ≥ 1 is a (p, k)-limit of Y, then Y has a nonempty subset of deficit at most 2 k + 2 all of whose points are (32768 k p, 194 k)-limits of X (exists_mirror_set). This is the analogue, in the setting of Section 4 of [Kor26], of Korten's strong mirror-set lemma Korten, Lemma 5; the constants 32768 and 194 are the ones of this proof.

The proof follows Korten's. By the entropy lemma for fibers, the light-patterns lemma and the conditional sampling law, modifying a uniform point of X first on a random mask of rate p and then on a random mask of rate q = 32768 k p rarely leaves a point whose fiber in X has density below 2 ^ (-194 k). For the first modification, a guiding distribution, which on dense fibers samples uniformly from their intersection with Y, replaces Korten's fixed-size guiding sets. It has density at most 2 ^ k and lands in Y with probability at least 3 / 4, so it gives mass at least 1 / 4 to the points of Y that are (q, 194 k)-limits of X, and these points are many.

Main definitions

• Cslib.BitString.IsDensityLimit: density limits Korten, Definition 2.

Main results

• Cslib.BitString.IsDensityLimit.exists_mem_apply_eq: a density limit of Y at a rate below 3 / 4 agrees with a point of Y at every coordinate.
• Cslib.BitString.exists_mirror_set: the strong mirror-set lemma, with the constants 32768 and 194.

References

• O. Korten, Top-Down Lower Bounds for All Depths

def Cslib.BitString.IsDensityLimit {ι : Type u_1} [Fintype ι] [DecidableEq ι] (Y : Finset (ι → Bool)) (p k : ℝ) (x : ι → Bool) : Prop

A (p,k)-limit point of Y Korten, Definition 2: with probability at least 3/4, the rate-p coordinate fiber over x has density at least 2^(-k) in Y.

@[instance_reducible]

noncomputable instance Cslib.BitString.instDecidablePredForallBoolIsDensityLimit {ι : Type u_1} [Fintype ι] [DecidableEq ι] (Y : Finset (ι → Bool)) (p k : ℝ) : DecidablePred (IsDensityLimit Y p k)

Being a density limit of Y is decidable, classically, as a real inequality.

theorem Cslib.BitString.IsDensityLimit.exists_mem_apply_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Y : Finset (ι → Bool)} {p k : ℝ} {x : ι → Bool} (hlim : IsDensityLimit Y p k x) (hp : 0 ≤ p) (hp' : p < 3 / 4) (i : ι) : ∃ y ∈ Y, y i = x i

A density limit at a rate below 3 / 4 agrees with a point of Y at every coordinate.

theorem Cslib.BitString.IsDensityLimit.mono_deficit {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Y : Finset (ι → Bool)} {p k k' : ℝ} {x : ι → Bool} (hlim : IsDensityLimit Y p k x) (hp : 0 ≤ p) (hp' : p ≤ 1) (hkk' : k ≤ k') : IsDensityLimit Y p k' x

A density limit with deficit k is one with every larger deficit.

Completion densities after two modifications

Apply the entropy lemma and the light-patterns lemma inside the fiber over the union of the two masks. The conditional sampling law then yields the 31 / 32 estimate for the fraction of first modifications with low completion density. The explicit constants are q = 32768 k p and the completion deficit 194 k.

The guiding distribution

On a sufficiently dense fiber, sample uniformly from its intersection with Y; on the remaining fibers, sample uniformly from the whole fiber. The density of this sampling rule is at most 2^k. This is a distributional variant of the fixed-size guiding sets in Korten's proof, avoiding a rounding operation. The completion estimate bounds the guided failure probability by 1/16, and intersecting Y with the (q, 194 k)-limits of X gives a nonempty mirror set of deficit at most 2 k + 2, with q = 32768 k p.

theorem Cslib.BitString.exists_mirror_set {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X Y : Finset (ι → Bool)) (hX : X.Nonempty) {k p q : ℝ} (hk : 1 ≤ k) (hdef : uniformDeficit X ≤ k) (hp : 0 < p) (hq : q = 32768 * k * p) (hq' : q ≤ 1 / 2) (hlim : ∀ x ∈ X, IsDensityLimit Y p k x) : ∃ Y' ⊆ Y, Y'.Nonempty ∧ uniformDeficit Y' ≤ 2 * k + 2 ∧ ∀ y ∈ Y', IsDensityLimit X q (194 * k) y

The strong mirror-set lemma Korten, Lemma 5 and Section 4, with the constants of this proof: if every point of a nonempty set X of deficit at most k ≥ 1 is a (p, k)-limit of Y, for a rate p > 0 with q = 32768 k p ≤ 1 / 2, then Y has a nonempty subset of deficit at most 2 k + 2 all of whose points are (q, 194 k)-limits of X.