From flat lossless witnesses to weighted strong condensation

Decompose the input into exact-size flat sources. For each component and seed, push uniform weights through the supplied injection. Their mixture is normalized and preserves the point-mass cap at every seed. Linearity of joint tests transfers the common error, and the equal-mass test criterion converts it to total variation.

theorem Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededCondenser_of_weightedStrong {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] [Fintype Ω] [Nonempty Seed] [Nonempty Ω] {E : α → Seed → Ω} {K : ℕ} {ε : ℝ} (extract : WeightedStrongSeededExtractor E K ε) : WeightedStrongSeededCondenser E K (Fintype.card Ω) ε

theorem Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededCondenser_of_flat_injections {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] [Fintype Ω] [Nonempty Seed] (C : α → Seed → Ω) {K : ℕ} (positive : 0 < K) {ε : ℝ} (flat : ∀ (P : Finset α), P.card = K → ∃ (g : Seed → ↥P ↪ Ω), ∀ (T : Finset (Seed × Ω)), |seededTestProb (fun (x : ↥P) => C ↑x) T - seededTestProb (fun (x : ↥P) (y : Seed) => (g y) x) T| ≤ ε) : WeightedStrongSeededCondenser C K K ε