Source thresholds and output projections for strong extractors #
Increasing the source cap threshold and discarding output coordinates preserve the same retained-seed error. Boolean truncation keeps precisely the first requested coordinates, including an empty prefix or the whole output. No positive source threshold or nonempty seed alphabet is required.
theorem
Algebraic.Cutwidth.Extractor.WeightedStrongSeededExtractor.mono_threshold
{α : Type u_1}
{Seed : Type u_2}
{Ω : Type u_3}
[Fintype α]
[Fintype Seed]
[Fintype Ω]
{E : α → Seed → Ω}
{K L : ℕ}
{ε : ℝ}
(extract : WeightedStrongSeededExtractor E K ε)
(threshold : K ≤ L)
:
A stronger source cap preserves the weighted strong-extractor guarantee.
theorem
Algebraic.Cutwidth.Extractor.WeightedStrongSeededExtractor.fst
{α : Type u_1}
{Seed : Type u_2}
{Ω : Type u_3}
{Tail : Type u_4}
[Fintype α]
[Fintype Seed]
[Fintype Ω]
[Fintype Tail]
[Nonempty Tail]
{E : α → Seed → Ω × Tail}
{K : ℕ}
{ε : ℝ}
(extract : WeightedStrongSeededExtractor E K ε)
:
WeightedStrongSeededExtractor (fun (a : α) (y : Seed) => (E a y).1) K ε
Dropping a nonempty finite output factor preserves strong extraction with the same error.
theorem
Algebraic.Cutwidth.Extractor.WeightedStrongSeededExtractor.truncate
{α : Type u_1}
{Seed : Type u_2}
[Fintype α]
[Fintype Seed]
{b M K : ℕ}
{ε : ℝ}
{E : α → Seed → Fin M → Bool}
(extract : WeightedStrongSeededExtractor E K ε)
(size : b ≤ M)
:
WeightedStrongSeededExtractor (fun (a : α) (y : Seed) (j : Fin b) => E a y (Fin.castLE size j)) K ε
Keeping the first b of M output bits preserves the source threshold and strong error.