Strong extraction under seed and output equivalences #
A bijective seed representation preserves uniform sampling, and a bijective output representation preserves the uniform output law. Reindexing retained seed-output tests therefore transfers the weighted strong-extractor guarantee with exactly the same source cap and error. Empty finite types are included.
theorem
Algebraic.Cutwidth.Extractor.WeightedStrongSeededExtractor.equiv
{α : Type u_1}
{Seed : Type u_2}
{Seed' : Type u_3}
{Ω : Type u_4}
{Ω' : Type u_5}
[Fintype α]
[Fintype Seed]
[Fintype Seed']
[Fintype Ω]
[Fintype Ω']
{E : α → Seed → Ω}
{K : ℕ}
{ε : ℝ}
(extract : WeightedStrongSeededExtractor E K ε)
(seed : Seed' ≃ Seed)
(output : Ω ≃ Ω')
:
WeightedStrongSeededExtractor (fun (a : α) (y : Seed') => output (E a (seed y))) K ε
Equivalent seed and output alphabets preserve weighted strong extraction without error loss.