Transporting condenser witnesses through injective output maps #
Push each ideal conditional distribution through the supplied injection. Normalization and the cap are preserved, and deterministic processing contracts each conditional distance before averaging over the retained seed.
theorem
Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededCondenser_map_output_injective
{α : Type u_1}
{Seed : Type u_2}
{Ω : Type u_3}
{Γ : Type u_4}
[Fintype α]
[Fintype Seed]
[Fintype Ω]
[Fintype Γ]
{C : α → Seed → Ω}
{Kin Kout : ℕ}
{ε : ℝ}
(cond : WeightedStrongSeededCondenser C Kin Kout ε)
(f : Seed → Ω → Γ)
(injective : ∀ (y : Seed), Function.Injective (f y))
:
WeightedStrongSeededCondenser (fun (x : α) (y : Seed) => f y (C x y)) Kin Kout ε