Strong extraction with an average leakage budget

A joint point-mass envelope p (tag, x) ≤ μ tag suffices for extraction retaining both the entire tag and the independent uniform seed. The error is at most the extractor error plus K * ∑ tag, μ tag. No bound on each normalized conditional row is assumed; zero-mass rows contribute zero.

This finite row estimate supplies the average conditional-entropy step used in Chattopadhyay and Liao, Extractors for Sum of Two Sources, Lemma 3.26, p. 15: https://arxiv.org/pdf/2110.12652. The independence-merging argument and the affine correlation-breaker applications in Chattopadhyay, Goodman, and Liao, https://eccc.weizmann.ac.il/report/2021/075/, are separate layers.

theorem Algebraic.Cutwidth.Extractor.WeightedStrongSeededExtractor.leakage_dist_le {Tag : Type u_1} {Source : Type u_2} {Seed : Type u_3} {Out : Type u_4} [Fintype Tag] [Fintype Source] [Fintype Seed] [Fintype Out] [Nonempty Seed] [Nonempty Out] {E : Source → Seed → Out} {K : ℕ} {ε : ℝ} (extract : WeightedStrongSeededExtractor E K ε) (error : 0 ≤ ε) (p : Tag × Source → ℝ) (probability : IsProbabilityWeight p) (μ : Tag → ℝ) (nonnegative : ∀ (t : Tag), 0 ≤ μ t) (cap : ∀ (t : Tag) (x : Source), p (t, x) ≤ μ t) : weightDist (weightedSeededOutput p fun (tx : Tag × Source) (y : Seed) => (tx.1, E tx.2 y)) (seedFamilyWeight fun (x : Seed) => uniformExtensionWeight Out (firstWeight p)) ≤ ε + ↑K * ∑ t : Tag, μ t

A joint row envelope gives extraction retaining the full leakage tag and uniform seed.

theorem Algebraic.Cutwidth.Extractor.WeightedStrongSeededExtractor.leakage_average_dist_le {Tag : Type u_1} {Source : Type u_2} {Seed : Type u_3} {Out : Type u_4} [Fintype Tag] [Fintype Source] [Fintype Seed] [Fintype Out] [Nonempty Seed] [Nonempty Out] {E : Source → Seed → Out} {K : ℕ} {ε : ℝ} (extract : WeightedStrongSeededExtractor E K ε) (error : 0 ≤ ε) (p : Tag × Source → ℝ) (probability : IsProbabilityWeight p) (μ : Tag → ℝ) (nonnegative : ∀ (t : Tag), 0 ≤ μ t) (cap : ∀ (t : Tag) (x : Source), p (t, x) ≤ μ t) : (∑ y : Seed, weightDist (mapWeight (fun (tx : Tag × Source) => (tx.1, E tx.2 y)) p) (uniformExtensionWeight Out (firstWeight p))) / ↑(Fintype.card Seed) ≤ ε + ↑K * ∑ t : Tag, μ t

The same leakage guarantee as the average distance over the independent uniform seed.