Extraction after two-sided finite leakage

The uniform-seed source retains a joint-mass envelope enlarged only by the extra leak's alphabet. Both actual and ideal seed laws average the same bounded discrepancy statistic. The bounded-statistic distance inequality charges the seed error once while preserving the actual retained marginal.

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

theorem Algebraic.Cutwidth.Extractor.Internal.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)) ≤ ε + δ + ρ