Bounded statistics and the distance form of strong extraction

Center a statistic in [0,1] at one half; equal total masses cancel the constant contribution. The finite-test characterization then identifies weighted strong extraction with distance from the uniform joint law.

theorem Algebraic.Cutwidth.Extractor.Internal.weightExpectation_sub_le_dist {α : Type u_1} [Fintype α] (p q f : α → ℝ) (mass : ∑ x : α, p x = ∑ x : α, q x) (lower : ∀ (x : α), 0 ≤ f x) (upper : ∀ (x : α), f x ≤ 1) : |∑ x : α, p x * f x - ∑ x : α, q x * f x| ≤ weightDist p q

theorem Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededExtractor_dist_le {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] [Fintype Ω] [Nonempty Seed] [Nonempty Ω] {E : α → Seed → Ω} {K : ℕ} {ε : ℝ} (extract : WeightedStrongSeededExtractor E K ε) {p : α → ℝ} (probability : IsProbabilityWeight p) (cap : CappedWeight p K) : weightDist (weightedSeededOutput p E) (seedFamilyWeight fun (x : Seed) => uniformWeight Ω) ≤ ε

theorem Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededExtractor_iff_dist_le {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] [Fintype Ω] [Nonempty Seed] [Nonempty Ω] (E : α → Seed → Ω) (K : ℕ) (ε : ℝ) : WeightedStrongSeededExtractor E K ε ↔ ∀ (p : α → ℝ), IsProbabilityWeight p → CappedWeight p K → weightDist (weightedSeededOutput p E) (seedFamilyWeight fun (x : Seed) => uniformWeight Ω) ≤ ε