Seeded randomness extractors

A (k, ε)-extractor ext : Input → Seed → Output turns every source of min-entropy at least k, together with an independent uniform seed, into an output within statistical distance ε of uniform (Cslib.Probability.IsExtractor). It is strong if the output stays ε-close to uniform even when the seed is revealed: the pair (seed, ext x seed) is ε-close to a uniform pair (Cslib.Probability.IsStrongExtractor) Nisan, Zuckerman, Vadhan, Chapter 6.

Strong extractors are extractors (IsStrongExtractor.isExtractor), and both notions apply to (k, δ)-sources at the cost of δ (IsExtractor.dist_le_of_isSource, IsStrongExtractor.dist_le_of_isSource).

The seed cannot be dropped. Without one, no function to Bool extracts even from sources missing only one bit of min-entropy: some output value has at least half of the inputs as preimages, and the uniform distribution on those inputs makes the output constant (not_isExtractor_bool_of_subsingleton) Vadhan, Chapter 6. Seeded extractors and two-source extractors are the two standard ways around this.

Main definitions

• Cslib.Probability.IsExtractor: (k, ε)-extractors.
• Cslib.Probability.IsStrongExtractor: strong (k, ε)-extractors, whose seed may be revealed.

Main results

• Cslib.Probability.IsStrongExtractor.isExtractor: strong extractors are extractors.
• Cslib.Probability.IsExtractor.dist_le_of_isSource, Cslib.Probability.IsStrongExtractor.dist_le_of_isSource: extraction from (k, δ)-sources.
• Cslib.Probability.not_isExtractor_bool_of_subsingleton: seedless extraction of one bit fails for sources missing one bit of min-entropy.

References

• N. Nisan, D. Zuckerman, Randomness is Linear in Space
• S. Vadhan, Pseudorandomness, Chapter 6

def Cslib.Probability.IsExtractor {Input : Type u_1} {Seed : Type u_2} {Output : Type u_3} [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output] (ext : Input → Seed → Output) (k ε : ℝ) : Prop

A (k, ε)-extractor: for every source of min-entropy at least k, applying ext to a sample of the source and an independent uniform seed gives an output within statistical distance ε of uniform.

def Cslib.Probability.IsStrongExtractor {Input : Type u_1} {Seed : Type u_2} {Output : Type u_3} [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output] (ext : Input → Seed → Output) (k ε : ℝ) : Prop

A strong (k, ε)-extractor: for every source of min-entropy at least k, the seed paired with the output of ext is within statistical distance ε of a uniform pair, so the output stays nearly uniform even given the seed.

theorem Cslib.Probability.IsExtractor.mono {Input : Type u_1} {Seed : Type u_2} {Output : Type u_3} [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output] {ext : Input → Seed → Output} {k k' ε ε' : ℝ} (h : IsExtractor ext k ε) (hk : k ≤ k') (hε : ε ≤ ε') : IsExtractor ext k' ε'

Extractors remain extractors for sources with more min-entropy and with more error.

theorem Cslib.Probability.IsStrongExtractor.mono {Input : Type u_1} {Seed : Type u_2} {Output : Type u_3} [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output] {ext : Input → Seed → Output} {k k' ε ε' : ℝ} (h : IsStrongExtractor ext k ε) (hk : k ≤ k') (hε : ε ≤ ε') : IsStrongExtractor ext k' ε'

Strong extractors remain strong extractors for sources with more min-entropy and with more error.

theorem Cslib.Probability.IsStrongExtractor.isExtractor {Input : Type u_1} {Seed : Type u_2} {Output : Type u_3} [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output] {ext : Input → Seed → Output} {k ε : ℝ} (h : IsStrongExtractor ext k ε) : IsExtractor ext k ε

Strong extractors are extractors: discarding the revealed seed cannot increase statistical distance.

theorem Cslib.Probability.IsExtractor.dist_le_of_isSource {Input : Type u_1} {Seed : Type u_2} {Output : Type u_3} [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output] {ext : Input → Seed → Output} {k ε : ℝ} [Fintype Input] (h : IsExtractor ext k ε) {source : PMF Input} {δ : NNReal} (hsource : PMF.IsSource source k δ) : dist (source.bind fun (x : Input) => PMF.map (fun (s : Seed) => ext x s) (PMF.uniformOfFintype Seed)) (PMF.uniformOfFintype Output) ≤ ↑δ + ε

Extraction from (k, δ)-sources. A (k, ε)-extractor applied to a (k, δ)-source gives an output within δ + ε of uniform.

theorem Cslib.Probability.IsStrongExtractor.dist_le_of_isSource {Input : Type u_1} {Seed : Type u_2} {Output : Type u_3} [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output] {ext : Input → Seed → Output} {k ε : ℝ} [Fintype Input] (h : IsStrongExtractor ext k ε) {source : PMF Input} {δ : NNReal} (hsource : PMF.IsSource source k δ) : dist (source.bind fun (x : Input) => PMF.map (fun (s : Seed) => (s, ext x s)) (PMF.uniformOfFintype Seed)) (PMF.uniformOfFintype (Seed × Output)) ≤ ↑δ + ε

Strong extraction from (k, δ)-sources. A strong (k, ε)-extractor applied to a (k, δ)-source gives a seed and output within δ + ε of a uniform pair.

Seedless extraction is impossible

theorem Cslib.Probability.not_isExtractor_bool_of_subsingleton {Input : Type u_1} {Seed : Type u_2} [Fintype Seed] [Nonempty Seed] {ε : ℝ} [Fintype Input] [Nonempty Input] [Subsingleton Seed] (ext : Input → Seed → Bool) (hε : ε < 1 / 2) : ¬IsExtractor ext (Real.logb 2 ↑(Fintype.card Input) - 1) ε

Seedless extraction fails. With a seed carrying no randomness, no function to Bool is a (log₂ |Input| - 1, ε)-extractor for ε < 1 / 2: some output value b has at least half of the inputs as preimages, and the uniform distribution on those inputs has min-entropy at least log₂ |Input| - 1 while its output is constantly b.