Extracting from concentrated conditional entropy

A source need not satisfy a pointwise probability bound everywhere. Discarding rare heavy outcomes yields a source to which leftover hashing applies, with explicit error for the discarded probability. This error is averaged over revealed side information, so rare observations do not need separate worst-case entropy assumptions.

IsTwoUniversal.leftover_hash_pi_conditional combines this bound with concentration. Independent samples with total conditional entropy H can be hashed with error at most 2 exp(-2 t^2 / (count * bound^2)) + sqrt(2 * |Output| * 2^(-(H - t))) / 2. The concentration term uses a bound on each sample's information content, supplied for uniform finite seeds by uniform_map_mass_ge.

Main results

• IsTwoUniversal.leftover_hash_of_heavy_probability: smooth a source by discarding heavy outcomes.
• IsTwoUniversal.leftover_hash_joint_of_heavy_probability: retain all public side information.
• IsTwoUniversal.leftover_hash_pi_conditional: extract from independent conditional sources.

References

• Thomas Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, TCC 2006, Section 3.3, Proposition 1 and Lemma 2. [Hol06]. We combine smoothing with the bounded-information concentration variant in EntropyConcentration; its loss depends on the uniform seed length rather than claiming Proposition 1's sharper alphabet-size bound.

Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the pinned finite-PMF metric.

theorem Cslib.Probability.IsTwoUniversal.leftover_hash_of_heavy_probability {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Finite Input] [Fintype Output] [Nonempty Output] {seed : PMF Seed} {hash : Seed → Input → Output} (hhash : IsTwoUniversal seed hash) (source : PMF Input) {mass : ℝ} (hmass : 0 ≤ mass) : dist (seededHash seed source hash) (seed.bind fun (s : Seed) => PMF.map (fun (x : Output) => (s, x)) (PMF.uniformOfFintype Output)) ≤ 2 * (source.toOuterMeasure {x : Input | mass < (source x).toReal}).toReal + √(↑(Fintype.card Output) * (2 * mass)) / 2

Heavy outcomes can be charged to extraction error. If their total probability is δ, hashing costs at most 2δ plus the leftover-hash error for a source with mass bound 2 * mass. No efficient sampler for the conditioned source is required by this statistical theorem.

theorem Cslib.Probability.IsTwoUniversal.leftover_hash_conditional_of_heavy_probability {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Finite 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) {mass : ℝ} (hmass : 0 ≤ mass) : 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))) ≤ 2 * ∑ info : Side, (side info).toReal * ((source info).toOuterMeasure {x : Input | mass < ((source info) x).toReal}).toReal + √(↑(Fintype.card Output) * (2 * mass)) / 2

With public side information, only the average probability of heavy conditional outcomes is charged to error. The seed and the side information are both retained in the comparison.

theorem Cslib.Probability.IsTwoUniversal.leftover_hash_joint_of_heavy_probability {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Finite Input] [Fintype Output] [Nonempty Output] {Side : Type u_4} [Fintype Side] {seed : PMF Seed} {hash : Seed → Input → Output} (hhash : IsTwoUniversal seed hash) (joint : PMF (Side × Input)) {mass : ℝ} (hmass : 0 ≤ mass) : dist (joint.bind fun (pair : Side × Input) => PMF.map (fun (s : Seed) => (pair.1, s, hash s pair.2)) seed) ((PMF.map Prod.fst joint).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))) ≤ 2 * (joint.toOuterMeasure {pair : Side × Input | mass < ((PMF.conditionalSnd joint pair.1) pair.2).toReal}).toReal + √(↑(Fintype.card Output) * (2 * mass)) / 2

The smoothed conditional leftover hash bound for a joint source. Both experiments preserve its public marginal and reveal the independent hash seed.

theorem Cslib.Probability.IsTwoUniversal.leftover_hash_pi_conditional {Seed : Type u_1} {Output : Type u_3} [Fintype Seed] [Fintype Output] [Nonempty Output] {ι : Type u_4} [Fintype ι] [DecidableEq ι] {α : ι → Type u_5} {β : ι → Type u_6} [(i : ι) → Fintype (α i)] [∀ (i : ι), Finite (β i)] {seed : PMF Seed} {hash : Seed → ((i : ι) → β i) → Output} (hhash : IsTwoUniversal seed hash) (joint : (i : ι) → PMF (α i × β i)) {bound ε : ℝ} (hbound : 0 ≤ bound) (hmass : ∀ (i : ι), ∀ pair ∈ (joint i).support, 2 ^ (-bound) ≤ ((joint i) pair).toReal) (hε : 0 ≤ ε) : dist ((PMF.pi joint).bind fun (outcome : (i : ι) → α i × β i) => PMF.map (fun (s : Seed) => (fun (i : ι) => (outcome i).1, s, hash s fun (i : ι) => (outcome i).2)) seed) ((PMF.pi fun (i : ι) => PMF.map Prod.fst (joint i)).bind fun (observed : (i : ι) → α i) => PMF.map (fun (x : Seed × Output) => (observed, x)) (seed.bind fun (s : Seed) => PMF.map (fun (x : Output) => (s, x)) (PMF.uniformOfFintype Output))) ≤ 2 * Real.exp (-2 * ε ^ 2 / (↑(Fintype.card ι) * bound ^ 2)) + √(↑(Fintype.card Output) * (2 * 2 ^ (-(∑ i : ι, PMF.conditionalEntropy (joint i) - ε)))) / 2

Independent joint samples supply almost their total conditional Shannon entropy to a two-universal extractor. The error separates the concentration loss from the leftover-hash loss; all observations and the complete hash seed remain public.