Perturbing a source-correlated seed

Independent-seed leakage extraction applies to the uniformized joint law. Deterministic processing pays the distance to that law once. Replacing its retained marginal by the actual retained marginal costs at most the same distance again, because uniformization contracts total variation.

theorem Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededExtractor_perturbed_seed_reference_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] {E : Source → Seed → Out} {K : ℕ} {ε δ : ℝ} (extract : WeightedStrongSeededExtractor E K ε) (error : 0 ≤ ε) (p : (Tag × Source) × Seed → ℝ) (probability : IsProbabilityWeight p) (μ : Tag → ℝ) (nonnegative : ∀ (t : Tag), 0 ≤ μ t) (cap : ∀ (t : Tag) (x : Source), firstWeight p (t, x) ≤ μ t) (seed : weightDist p (uniformSecondWeight p) ≤ δ) : weightDist (mapWeight (fun (txs : (Tag × Source) × Seed) => ((txs.1.1, txs.2), E txs.1.2 txs.2)) p) (uniformSecondWeight (mapWeight (fun (txs : (Tag × Source) × Seed) => ((txs.1.1, txs.2), E txs.1.2 txs.2)) (uniformSecondWeight p))) ≤ ε + δ + ↑K * ∑ t : Tag, μ t

theorem Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededExtractor_perturbed_seed_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] {E : Source → Seed → Out} {K : ℕ} {ε δ : ℝ} (extract : WeightedStrongSeededExtractor E K ε) (error : 0 ≤ ε) (p : (Tag × Source) × Seed → ℝ) (probability : IsProbabilityWeight p) (μ : Tag → ℝ) (nonnegative : ∀ (t : Tag), 0 ≤ μ t) (cap : ∀ (t : Tag) (x : Source), firstWeight p (t, x) ≤ μ t) (seed : weightDist p (uniformSecondWeight p) ≤ δ) : weightDist (mapWeight (fun (txs : (Tag × Source) × Seed) => ((txs.1.1, txs.2), E txs.1.2 txs.2)) p) (uniformSecondWeight (mapWeight (fun (txs : (Tag × Source) × Seed) => ((txs.1.1, txs.2), E txs.1.2 txs.2)) p)) ≤ ε + 2 * δ + ↑K * ∑ t : Tag, μ t