Extending strong extraction from flat to weighted sources

Seeded test probabilities are linear in the source weights. The exact decomposition into uniform fixed-size supports therefore transfers the flat-source guarantee without any error loss. Conversely every nonempty flat support is a normalized capped weighting on the ambient finite type.

theorem Algebraic.Cutwidth.Extractor.Internal.probabilityWeight_flatWeight {α : Type u_1} [Fintype α] (P : Finset α) (nonempty : P.Nonempty) : IsProbabilityWeight (flatWeight P)

theorem Algebraic.Cutwidth.Extractor.Internal.cappedWeight_flatWeight {α : Type u_1} (P : Finset α) {K : ℕ} (size : K ≤ P.card) : CappedWeight (flatWeight P) K

theorem Algebraic.Cutwidth.Extractor.Internal.weightedSeededTestProb_uniformWeight {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] (E : α → Seed → Ω) (T : Finset (Seed × Ω)) : weightedSeededTestProb (uniformWeight α) E T = seededTestProb E T

theorem Algebraic.Cutwidth.Extractor.Internal.weightedSeededTestProb_flatWeight {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] (E : α → Seed → Ω) (P : Finset α) (T : Finset (Seed × Ω)) : weightedSeededTestProb (flatWeight P) E T = seededTestProb (fun (x : ↥P) => E ↑x) T

theorem Algebraic.Cutwidth.Extractor.Internal.weightedSeededTestProb_mixture {α : Type u_1} {ι : Type u_2} {Seed : Type u_3} {Ω : Type u_4} [Fintype α] [Fintype ι] [Fintype Seed] (w : ι → ℝ) (p : ι → α → ℝ) (E : α → Seed → Ω) (T : Finset (Seed × Ω)) : weightedSeededTestProb (fun (x : α) => ∑ i : ι, w i * p i x) E T = ∑ i : ι, w i * weightedSeededTestProb (p i) E T

theorem Algebraic.Cutwidth.Extractor.Internal.weightedStrong_of_flat {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] [Fintype Ω] {E : α → Seed → Ω} {K : ℕ} {ε : ℝ} (extract : FlatStrongSeededExtractor E K ε) (positive : 0 < K) : WeightedStrongSeededExtractor E K ε

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