Bounded expectations and retained-seed statistical distance

For equal-mass real weights, every statistic valued in [0,1] changes by at most total variation distance. Normalized strong extraction is also equivalent to distance from the independent uniform seed-output law.

These elementary finite probability facts support the independence-merging argument of Chattopadhyay and Liao, Extractors for Sum of Two Sources, Lemma 3.26, p. 15: https://arxiv.org/pdf/2110.12652. That conditional independence argument is a separate layer.

theorem Algebraic.Cutwidth.Extractor.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

A statistic in [0,1] changes by at most the distance between equal-mass weights. Neither normalization nor nonnegativity of the weights is needed.

theorem Algebraic.Cutwidth.Extractor.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 Ω) ≤ ε

Strong extraction bounds distance from the independent uniform retained-seed law.

theorem Algebraic.Cutwidth.Extractor.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 Ω) ≤ ε

The finite-test and total-variation formulations of weighted strong extraction coincide.