Strong extraction with two-sided finite leakage

A shared transcript indexes independent left and right distributions. A joint source-mass envelope controls the left observation. The seed is close to uniform given the right observation. An additional finite leak may depend on both the left variable and that right observation. Extraction retains the entire right variable and both left leaks; its error is the extractor error, the seed discrepancy, and the envelope total times the leak's alphabet size.

The bound permits arbitrary low-entropy transcript fibers. It is the finite weighted form underlying the independence-merging lemma in Chattopadhyay--Liao, Extractors for Sum of Two Sources (2021), Lemma 3.26 (printed p.15), used in Theorem 6.1 (pp.22--25): https://arxiv.org/abs/2110.12652. That lemma credits Chattopadhyay--Goodman--Liao and ideas of Chattopadhyay--Li. No correlation-breaker algorithm is assumed or constructed in this probability layer.

theorem Algebraic.Cutwidth.Extractor.twoSidedExtractionWeight_eq_map {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} {Seed : Type u_5} {Out : Type u_6} {U : Type u_7} {V : Type u_8} {W : Type u_9} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x : Z → A → X) (y : Z → B → Seed) (u : Z → A → U) (v : Z → B → V) (leak : Z → V → A → W) (E : X → Seed → Out) : twoSidedExtractionWeight w l r x y u v leak E = mapWeight (fun (p : (Z × B) × A) => ((p.1, u p.1.1 p.2, leak p.1.1 (v p.1.1 p.1.2) p.2), E (x p.1.1 p.2) (y p.1.1 p.1.2))) (factoredWeight w l r)

The retained extraction law is the actual deterministic image of the factored source.

theorem Algebraic.Cutwidth.Extractor.twoSidedExtractionWeight_probability {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} {Seed : Type u_5} {Out : Type u_6} {U : Type u_7} {V : Type u_8} {W : Type u_9} [Fintype Z] [Fintype A] [Fintype B] [Fintype Out] [Fintype U] [Fintype W] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x : Z → A → X) (y : Z → B → Seed) (u : Z → A → U) (v : Z → B → V) (leak : Z → V → A → W) (E : X → Seed → Out) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (twoSidedExtractionWeight w l r x y u v leak E)

Normalized factored sources give a normalized retained extraction law.

theorem Algebraic.Cutwidth.Extractor.WeightedStrongSeededExtractor.two_sided_leakage_dist_le {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} {Seed : Type u_5} {Out : Type u_6} {U : Type u_7} {V : Type u_8} {W : Type u_9} [Fintype Z] [Fintype A] [Fintype B] [Fintype X] [Fintype Seed] [Fintype Out] [Fintype U] [Fintype V] [Fintype W] [Nonempty Seed] [Nonempty Out] {E : X → Seed → Out} {K : ℕ} {ε δ : ℝ} (extract : WeightedStrongSeededExtractor E K ε) (error : 0 ≤ ε) (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x : Z → A → X) (y : Z → B → Seed) (u : Z → A → U) (v : Z → B → V) (leak : Z → V → A → W) (μ : Z × U → ℝ) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (nonnegative : ∀ (t : Z × U), 0 ≤ μ t) (cap : ∀ (z : Z) (u₀ : U) (x₀ : X), w z * mapWeight (fun (a : A) => (u z a, x z a)) (l z) (u₀, x₀) ≤ μ (z, u₀)) (seed : weightDist (observedSeedWeight w r v y) (uniformSecondWeight (observedSeedWeight w r v y)) ≤ δ) : weightDist (twoSidedExtractionWeight w l r x y u v leak E) (uniformSecondWeight (twoSidedExtractionWeight w l r x y u v leak E)) ≤ ε + δ + ↑K * ↑(Fintype.card W) * ∑ t : Z × U, μ t

A joint-mass envelope pays for finite leakage without a cap on each conditional source.

theorem Algebraic.Cutwidth.Extractor.WeightedStrongSeededExtractor.two_sided_leakage_dist_le_of_budget {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} {Seed : Type u_5} {Out : Type u_6} {U : Type u_7} {V : Type u_8} {W : Type u_9} [Fintype Z] [Fintype A] [Fintype B] [Fintype X] [Fintype Seed] [Fintype Out] [Fintype U] [Fintype V] [Fintype W] [Nonempty Seed] [Nonempty Out] {E : X → Seed → Out} {K : ℕ} {ε δ ρ : ℝ} (extract : WeightedStrongSeededExtractor E K ε) (error : 0 ≤ ε) (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x : Z → A → X) (y : Z → B → Seed) (u : Z → A → U) (v : Z → B → V) (leak : Z → V → A → W) (μ : Z × U → ℝ) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (nonnegative : ∀ (t : Z × U), 0 ≤ μ t) (cap : ∀ (z : Z) (u₀ : U) (x₀ : X), w z * mapWeight (fun (a : A) => (u z a, x z a)) (l z) (u₀, x₀) ≤ μ (z, u₀)) (seed : weightDist (observedSeedWeight w r v y) (uniformSecondWeight (observedSeedWeight w r v y)) ≤ δ) (budget : ↑K * ↑(Fintype.card W) * ∑ t : Z × U, μ t ≤ ρ) : weightDist (twoSidedExtractionWeight w l r x y u v leak E) (uniformSecondWeight (twoSidedExtractionWeight w l r x y u v leak E)) ≤ ε + δ + ρ

A budget on the average joint envelope gives an additive leakage error.