Normalization of the finite leftover-hash bound #
The counting proof is normalized to the existing retained-seed test probability. Restricting an input family along an injection preserves universality, so the finite-type bound applies to every finite flat support.
theorem
Algebraic.Cutwidth.Extractor.Internal.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
theorem
Algebraic.Cutwidth.Extractor.Internal.seededTestProb_sub_uniform_mul
{α : Type u_1}
{Seed : Type u_2}
{Ω : Type u_3}
[Fintype α]
[Fintype Seed]
[Fintype Ω]
[Nonempty α]
[Nonempty Seed]
[Nonempty Ω]
(E : α → Seed → Ω)
(T : Finset (Seed × Ω))
:
(seededTestProb E T - uniformSeededTestProb T) * (↑(Fintype.card α) * ↑(Fintype.card Seed) * ↑(Fintype.card Ω)) = ∑ z ∈ T, hashCenteredCount E z
theorem
Algebraic.Cutwidth.Extractor.Internal.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 × Ω))
:
theorem
Algebraic.Cutwidth.Extractor.Internal.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)
theorem
Algebraic.Cutwidth.Extractor.Internal.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)
: