Injective output transport for strong condensers #
An injective representation of each output preserves the conditional point-mass cap and cannot increase statistical distance. The representation may depend on the retained seed. No extra randomness or error is introduced. The theorem also covers an empty seed type under the zero-mass convention.
theorem
Algebraic.Cutwidth.Extractor.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 ε
Injective output encoding preserves both entropy thresholds and the joint error bound.