Finite independence merging for overlapping tampering sets

Source copies indexed by T enter a joint point-mass envelope. The actual seed is close to uniform given the transcript and seed copies indexed by S. Extraction then remains close to uniform given the transcript, every seed, and all tampered outputs in S ∪ T. The sets need not be disjoint.

The exact leakage cost is K * |Out| ^ |S| * ∑ μ. Bounding that cost by the extractor error gives 2 * ε + δ. This is the finite envelope form of Chattopadhyay--Liao, Extractors for Sum of Two Sources, Lemma 3.26, p.15, https://arxiv.org/pdf/2110.12652. That source credits Chattopadhyay--Goodman--Liao and ideas of Chattopadhyay--Li. Here conditional independence is expressed by explicit normalized factored laws; no logarithmic entropy definition or correlation-breaker construction is introduced.

theorem Algebraic.Cutwidth.Extractor.WeightedStrongSeededExtractor.independence_merging_dist_le {Z : Type u_1} {X : Type u_2} {Seed : Type u_3} {Out : Type u_4} {t : ℕ} [Fintype Z] [Fintype X] [Fintype Seed] [Fintype Out] [Nonempty Seed] [Nonempty Out] {E : X → Seed → Out} {K : ℕ} {ε δ : ℝ} (extract : WeightedStrongSeededExtractor E K ε) (error : 0 ≤ ε) (w : Z → ℝ) (l : Z → X × (Fin t → X) → ℝ) (r : Z → Seed × (Fin t → Seed) → ℝ) (S T : Finset (Fin t)) (μ : Z × (↥T → X) → ℝ) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (nonnegative : ∀ (zu : Z × (↥T → X)), 0 ≤ μ zu) (cap : ∀ (z : Z) (u : ↥T → X) (x : X), w z * mapWeight (fun (a : X × (Fin t → X)) => (fun (j : ↥T) => a.2 ↑j, a.1)) (l z) (u, x) ≤ μ (z, u)) (seed : weightDist (observedSeedWeight w r (fun (x : Z) (b : Seed × (Fin t → Seed)) (j : ↥S) => b.2 ↑j) fun (x : Z) (b : Seed × (Fin t → Seed)) => b.1) (uniformSecondWeight (observedSeedWeight w r (fun (x : Z) (b : Seed × (Fin t → Seed)) (j : ↥S) => b.2 ↑j) fun (x : Z) (b : Seed × (Fin t → Seed)) => b.1)) ≤ δ) : weightDist (independenceMergingWeight w l r E S T) (uniformSecondWeight (independenceMergingWeight w l r E S T)) ≤ ε + δ + ↑K * ↑(Fintype.card Out) ^ S.card * ∑ zu : Z × (↥T → X), μ zu

Merge source-side and seed-side independence, retaining every seed and the selected outputs.

theorem Algebraic.Cutwidth.Extractor.WeightedStrongSeededExtractor.independence_merging_dist_le_of_budget {Z : Type u_1} {X : Type u_2} {Seed : Type u_3} {Out : Type u_4} {t : ℕ} [Fintype Z] [Fintype X] [Fintype Seed] [Fintype Out] [Nonempty Seed] [Nonempty Out] {E : X → Seed → Out} {K : ℕ} {ε δ : ℝ} (extract : WeightedStrongSeededExtractor E K ε) (error : 0 ≤ ε) (w : Z → ℝ) (l : Z → X × (Fin t → X) → ℝ) (r : Z → Seed × (Fin t → Seed) → ℝ) (S T : Finset (Fin t)) (μ : Z × (↥T → X) → ℝ) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (nonnegative : ∀ (zu : Z × (↥T → X)), 0 ≤ μ zu) (cap : ∀ (z : Z) (u : ↥T → X) (x : X), w z * mapWeight (fun (a : X × (Fin t → X)) => (fun (j : ↥T) => a.2 ↑j, a.1)) (l z) (u, x) ≤ μ (z, u)) (seed : weightDist (observedSeedWeight w r (fun (x : Z) (b : Seed × (Fin t → Seed)) (j : ↥S) => b.2 ↑j) fun (x : Z) (b : Seed × (Fin t → Seed)) => b.1) (uniformSecondWeight (observedSeedWeight w r (fun (x : Z) (b : Seed × (Fin t → Seed)) (j : ↥S) => b.2 ↑j) fun (x : Z) (b : Seed × (Fin t → Seed)) => b.1)) ≤ δ) (budget : ↑K * ↑(Fintype.card Out) ^ S.card * ∑ zu : Z × (↥T → X), μ zu ≤ ε) : weightDist (independenceMergingWeight w l r E S T) (uniformSecondWeight (independenceMergingWeight w l r E S T)) ≤ 2 * ε + δ

Paying at most one extractor error for leakage gives the 2ε + δ merging bound.