Projecting weighted strong-extractor outputs #
Threshold monotonicity uses source nonnegativity directly. Product projection pulls a joint test back to its product with the discarded alphabet, so the uniform comparison is unchanged. Splitting a Boolean vector into a prefix and suffix then gives exact prefix truncation.
theorem
Algebraic.Cutwidth.Extractor.Internal.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 ε
theorem
Algebraic.Cutwidth.Extractor.Internal.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 ε