Robust extraction from an approximately independent uniform seed

The seed may be correlated with both the source and its retained tag. Its distance from the law obtained by making that seed independently uniform controls extraction with the actual tag and seed retained. An average joint source-mass envelope suffices; no conditional source cap is assumed.

The actual-marginal bound charges the seed discrepancy twice. A comparison with the reference law's retained marginal charges it once. This finite stability deduction combines the existing leakage bound with deterministic contraction and the triangle inequality. It supports alternating extraction in the affine correlation-breaker argument of Chattopadhyay--Liao, Extractors for Sum of Two Sources, Theorem 6.1, https://arxiv.org/pdf/2110.12652; the alternating program is a separate layer.

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

Approximate joint seed uniformity gives extraction retaining the actual tag/seed marginal.

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

Comparing against the independent-seed reference marginal pays the seed discrepancy once.