Strong extractors from universal hashing

The leftover hash lemma, read as a statement about extractors: if hash is a two-universal family under the uniform seed, then ext x s = hash s x is a strong (k, ε)-extractor with ε = √(|Output| · 2⁻ᵏ) / 2 (IsTwoUniversal.isStrongExtractor). If log₂ |Output| + 2 log₂ (1 / δ) ≤ k, the error is at most δ / 2 (IsTwoUniversal.isStrongExtractor_of_logb_le), so universal hashing extracts all but 2 log₂ (1 / δ) bits of the min-entropy Vadhan, Chapter 6, Håstad, Impagliazzo, Levin, Luby. More generally, an ε-universal family gives error √(|Output| · (2⁻ᵏ + ε) - 1) / 2 (IsUniversalHash.isStrongExtractor).

A uniformly random Boolean m × n matrix is a two-universal family, so multiplying by it is a strong extractor from n-bit sources of min-entropy at least m + 2 log₂ (1 / δ) to m bits with error δ / 2 and an m n-bit seed (BitString.LinearHash.isStrongExtractor).

Main results

• Cslib.Probability.IsTwoUniversal.isStrongExtractor: the leftover hash lemma as a strong extractor.
• Cslib.Probability.IsTwoUniversal.isStrongExtractor_of_logb_le: its entropy-loss form.
• Cslib.Probability.IsUniversalHash.isStrongExtractor: the same for ε-universal families.
• Cslib.BitString.LinearHash.isStrongExtractor: Boolean matrix multiplication is a strong extractor.

References

• S. Vadhan, Pseudorandomness, Chapter 6
• J. Håstad, R. Impagliazzo, L. Levin, M. Luby, A Pseudorandom Generator from any One-way Function

theorem Cslib.Probability.IsTwoUniversal.isStrongExtractor {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Nonempty Seed] [Finite Input] [Fintype Output] [Nonempty Output] {hash : Seed → Input → Output} (hhash : IsTwoUniversal (PMF.uniformOfFintype Seed) hash) (k : ℝ) : IsStrongExtractor (fun (x : Input) (s : Seed) => hash s x) k (√(↑(Fintype.card Output) * 2 ^ (-k)) / 2)

The leftover hash lemma as a strong extractor. A two-universal family under the uniform seed is a strong (k, √(|Output| · 2⁻ᵏ) / 2)-extractor.

theorem Cslib.Probability.IsTwoUniversal.isStrongExtractor_of_logb_le {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Nonempty Seed] [Finite Input] [Fintype Output] [Nonempty Output] {hash : Seed → Input → Output} (hhash : IsTwoUniversal (PMF.uniformOfFintype Seed) hash) {δ : ℝ} (hδ : 0 < δ) {k : ℝ} (hk : Real.logb 2 ↑(Fintype.card Output) + 2 * Real.logb 2 δ⁻¹ ≤ k) : IsStrongExtractor (fun (x : Input) (s : Seed) => hash s x) k (δ / 2)

Entropy loss of hashing. If log₂ |Output| + 2 log₂ (1 / δ) ≤ k, a two-universal family under the uniform seed is a strong (k, δ / 2)-extractor.

theorem Cslib.Probability.IsUniversalHash.isStrongExtractor {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Nonempty Seed] [Finite Input] [Fintype Output] [Nonempty Output] {hash : Seed → Input → Output} {ε : ENNReal} (hhash : IsUniversalHash (PMF.uniformOfFintype Seed) hash ε) (hε : ε ≠ ⊤) (k : ℝ) : IsStrongExtractor (fun (x : Input) (s : Seed) => hash s x) k (√(↑(Fintype.card Output) * (2 ^ (-k) + ε.toReal) - 1) / 2)

ε-universal hashing as a strong extractor. An ε-universal family under the uniform seed is a strong (k, √(|Output| · (2⁻ᵏ + ε) - 1) / 2)-extractor. For ε = 1 / |Output| this is the two-universal bound IsTwoUniversal.isStrongExtractor.

theorem Cslib.BitString.LinearHash.isStrongExtractor (n m : ℕ) {δ : ℝ} (hδ : 0 < δ) {k : ℝ} (hk : ↑m + 2 * Real.logb 2 δ⁻¹ ≤ k) : Probability.IsStrongExtractor (fun (x : BitString n) (rows : Fin m → BitString n) => hash rows x) k (δ / 2)

Boolean matrix multiplication is a strong extractor. Multiplying an n-bit source of min-entropy at least m + 2 log₂ (1 / δ) by a uniformly random Boolean m × n matrix gives m bits within statistical distance δ / 2 of uniform, even given the matrix.