Transporting the scheduled condenser to weighted inputs

An injective representation preserves exact support cardinality and uniform test probabilities. Transport the scheduled condenser's seedwise injection witnesses along that equivalence, then apply the finite flat-mixture theorem.

theorem Algebraic.Cutwidth.Extractor.Internal.decodedExplicitCondenser_weighted (n k e u : ℕ) {α : Type u_1} [Fintype α] [Fintype (AdjoinRoot (binaryModulus (sparseFieldExponent u (explicitCondenserBudget n k e))))] (rate : 0 < u) (input : α ↪ List Bool) (source : ∀ (x : α), (input x).length = n) : WeightedStrongSeededCondenser (fun (x : α) => decodedExplicitCondenser n k e u (input x)) (2 ^ k) (2 ^ k) (2 ^ e)⁻¹

theorem Algebraic.Cutwidth.Extractor.Internal.decodedExplicitCondenser_weighted_ofFn (n k e u : ℕ) [Fintype (AdjoinRoot (binaryModulus (sparseFieldExponent u (explicitCondenserBudget n k e))))] (rate : 0 < u) : WeightedStrongSeededCondenser (fun (x : Fin n → Bool) => decodedExplicitCondenser n k e u (List.ofFn x)) (2 ^ k) (2 ^ k) (2 ^ e)⁻¹