Leftover hashing from weak random sources

The leftover hash lemma for (k, ε)-sources: hashing a (k, ε)-source with an independent two-universal seed, which stays public, gives a distribution within ε + √(|Output| · 2⁻ᵏ) / 2 of the seed paired with an independent uniform value. With log₂ |Output| + 2 log₂ (1 / δ) ≤ k the error is at most ε + δ / 2, so a two-universal family is a strong extractor that loses 2 log₂ (1 / δ) bits of min-entropy Vadhan, Chapter 6, Håstad, Impagliazzo, Levin, Luby. With public side information it suffices that every possible conditional source is a (k, ε)-source.

These are corollaries of the pointwise-mass form IsTwoUniversal.leftover_hash_of_mass_le and of dist_seededHash_le. Sources with rare heavy outcomes are (k, ε)-sources by Cslib.Probability.PMF.isSource_of_heavy_le; IsTwoUniversal.leftover_hash_of_heavy_probability states the resulting extraction bound directly.

Main results

• Cslib.Probability.IsTwoUniversal.leftover_hash_of_isSource: the leftover hash lemma for (k, ε)-sources.
• Cslib.Probability.IsTwoUniversal.leftover_hash_of_isSource_of_logb_le: the entropy-loss form.
• Cslib.Probability.IsTwoUniversal.leftover_hash_conditional_of_isSource: extraction with side information.

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.leftover_hash_of_isSource {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Input] [Fintype Output] [Nonempty Output] {seed : PMF Seed} {hash : Seed → Input → Output} (hhash : IsTwoUniversal seed hash) {source : PMF Input} {k : ℝ} {ε : NNReal} (hsource : PMF.IsSource source k ε) : dist (seededHash seed source hash) (seed.bind fun (s : Seed) => PMF.map (fun (x : Output) => (s, x)) (PMF.uniformOfFintype Output)) ≤ ↑ε + √(↑(Fintype.card Output) * 2 ^ (-k)) / 2

The leftover hash lemma for (k, ε)-sources. Hashing a (k, ε)-source with an independent two-universal seed, revealed in the output, is within ε + √(|Output| · 2⁻ᵏ) / 2 of the seed paired with an independent uniform value.

theorem Cslib.Probability.IsTwoUniversal.leftover_hash_of_isSource_of_logb_le {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Input] [Fintype Output] [Nonempty Output] {seed : PMF Seed} {hash : Seed → Input → Output} (hhash : IsTwoUniversal seed hash) {source : PMF Input} {k : ℝ} {ε : NNReal} (hsource : PMF.IsSource source k ε) {δ : ℝ} (hδ : 0 < δ) (hk : Real.logb 2 ↑(Fintype.card Output) + 2 * Real.logb 2 δ⁻¹ ≤ k) : dist (seededHash seed source hash) (seed.bind fun (s : Seed) => PMF.map (fun (x : Output) => (s, x)) (PMF.uniformOfFintype Output)) ≤ ↑ε + δ / 2

Entropy loss of leftover hashing. If the source is a (k, ε)-source with log₂ |Output| + 2 log₂ (1 / δ) ≤ k, hashing with an independent public two-universal seed is within ε + δ / 2 of the seed paired with an independent uniform value.

theorem Cslib.Probability.IsTwoUniversal.leftover_hash_conditional_of_isSource {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Input] [Fintype Output] [Nonempty Output] {Side : Type u_4} [Fintype Side] {seed : PMF Seed} {hash : Seed → Input → Output} (hhash : IsTwoUniversal seed hash) (side : PMF Side) {source : Side → PMF Input} {k : ℝ} {ε : NNReal} (hsource : ∀ info ∈ side.support, PMF.IsSource (source info) k ε) : dist (side.bind fun (info : Side) => PMF.map (fun (x : Seed × Output) => (info, x)) (seededHash seed (source info) hash)) (side.bind fun (info : Side) => PMF.map (fun (x : Seed × Output) => (info, x)) (seed.bind fun (s : Seed) => PMF.map (fun (x : Output) => (s, x)) (PMF.uniformOfFintype Output))) ≤ ↑ε + √(↑(Fintype.card Output) * 2 ^ (-k)) / 2

Leftover hashing with side information. If every possible conditional source is a (k, ε)-source, hashing with an independent two-universal seed hides the hash value up to ε + √(|Output| · 2⁻ᵏ) / 2, even when the side information and the seed are revealed.