Counting bad input fibres of a seeded extractor #
If at least K inputs each hit a small test on more than a 2ε fraction of
seeds, the uniform distribution on those inputs contradicts extraction.
Bounding each source point mass then gives sampling for arbitrary weak sources.
theorem
Algebraic.Cutwidth.Extractor.Internal.card_badInputs_lt
{α : Type u_1}
{Seed : Type u_2}
{Ω : Type u_3}
[Fintype α]
[Fintype Seed]
[Fintype Ω]
[Nonempty Seed]
[Nonempty Ω]
{E : α → Seed → Ω}
{K : ℕ}
{ε : ℝ}
(extract : FlatSeededExtractor E K ε)
(positive : 0 < K)
(T : Finset Ω)
(small : ↑T.card ≤ ε * ↑(Fintype.card Ω))
:
theorem
Algebraic.Cutwidth.Extractor.Internal.sampler_of_flatSeededExtractor
{α : Type u_1}
{Seed : Type u_2}
{Ω : Type u_3}
[Fintype α]
[Fintype Seed]
[Fintype Ω]
[Nonempty Seed]
[Nonempty Ω]
{E : α → Seed → Ω}
{K : ℕ}
{L ε δ : ℝ}
(extract : FlatSeededExtractor E K ε)
(positive : 0 < K)
(source : 0 < L)
(budget : ↑K ≤ δ * L)
:
Sampler E L ε δ
theorem
Algebraic.Cutwidth.Extractor.Internal.card_badInputs_inter_le
{α : Type u_1}
{Seed : Type u_2}
{Ω : Type u_3}
[Fintype α]
[Fintype Seed]
[Fintype Ω]
[Nonempty Seed]
[Nonempty Ω]
{E : α → Seed → Ω}
{K : ℕ}
{ε δ : ℝ}
(extract : FlatSeededExtractor E K ε)
(positive : 0 < K)
(P : Finset α)
(budget : ↑K ≤ δ * ↑P.card)
(T : Finset Ω)
(small : ↑T.card ≤ ε * ↑(Fintype.card Ω))
: