The finite retained-seed leftover-hash lemma

A universal hash family extracts from every finite flat source. For a support of cardinality N and an output type of cardinality M, every joint test of the seed and output has squared discrepancy at most M / (4 * N) from the independent uniform distribution. The factor 1/4 is included in the checked bound. Neither pairwise independence nor a uniform output for each fixed input is assumed.

The standard collision-to-second-moment argument is credited to the leftover-hash lemma, as presented in Guruswami, Umans, and Vadhan, Unbalanced Expanders and Randomness Extractors from Parvaresh--Vardy Codes, Section 5.1, Lemma 5.1, and Barak, Dodis, Krawczyk, Pereira, Pietrzak, Standaert, and Yu, Leftover Hash Lemma, Revisited, Definition 2 and Lemma 1. The proof here works directly with finite real sums and retained-seed tests.

• https://people.seas.harvard.edu/~salil/research/PVcondenser-jacm.pdf
• https://www.iacr.org/archive/crypto2011/68410001/68410001.pdf

theorem Algebraic.Cutwidth.Extractor.UniversalHashFamily.comp_injective {α : Type u_1} {β : Type u_2} {Seed : Type u_3} {Ω : Type u_4} [Fintype Seed] [Fintype Ω] {E : α → Seed → Ω} (universal : UniversalHashFamily E) (f : β → α) (injective : Function.Injective f) : UniversalHashFamily fun (x : β) (y : Seed) => E (f x) y

Restricting the input domain along an injection preserves universality.

theorem Algebraic.Cutwidth.Extractor.UniversalHashFamily.seededTestProb_sub_uniform_sq_le {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] [Fintype Ω] [Nonempty α] [Nonempty Seed] [Nonempty Ω] {E : α → Seed → Ω} (universal : UniversalHashFamily E) (T : Finset (Seed × Ω)) : (seededTestProb E T - uniformSeededTestProb T) ^ 2 ≤ ↑(Fintype.card Ω) / (4 * ↑(Fintype.card α))

The sharp squared leftover-hash bound for a uniform finite input type, against every joint test of the retained seed and output.

theorem Algebraic.Cutwidth.Extractor.UniversalHashFamily.flat_test_sq_le {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype Seed] [Fintype Ω] [Nonempty Seed] [Nonempty Ω] {E : α → Seed → Ω} (universal : UniversalHashFamily E) (P : Finset α) (nonempty : P.Nonempty) (T : Finset (Seed × Ω)) : (seededTestProb (fun (x : ↥P) => E ↑x) T - uniformSeededTestProb T) ^ 2 ≤ ↑(Fintype.card Ω) / (4 * ↑P.card)

The sharp squared leftover-hash bound for any nonempty finite flat support.

theorem Algebraic.Cutwidth.Extractor.UniversalHashFamily.flatStrongSeededExtractor {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype Seed] [Fintype Ω] [Nonempty Seed] [Nonempty Ω] {E : α → Seed → Ω} (universal : UniversalHashFamily E) {K : ℕ} {ε : ℝ} (positive : 0 < K) (error : 0 ≤ ε) (budget : ↑(Fintype.card Ω) ≤ 4 * ε ^ 2 * ↑K) : FlatStrongSeededExtractor E K ε

A universal family is a strong extractor whenever the output size fits the sharp leftover-hash error budget.