Reindexing retained-seed extractor tests #
Pull back each test along the product of the seed equivalence and inverse output equivalence. The filtered seed counts and both finite alphabet cardinalities are unchanged. No normalization by a positive denominator is needed, so empty alphabets retain the existing zero-division convention.
theorem
Algebraic.Cutwidth.Extractor.Internal.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 ε