Two-sided merging from a conditionally smooth uniform source

The honest source is close to uniform jointly with the transcript and a selected original left observation. A coupling repairs only that honest coordinate while preserving the complete original left state. Observing the actual original prefix then pays its alphabet size divided by the source alphabet size. Extraction keeps the full right state, selected left observation, prefix, and additional left leak. The repair costs the original distance once because this entire retained marginal is unchanged.

This is a finite weighted consumer for the smooth-source step in Chattopadhyay--Liao, Extractors for Sum of Two Sources (2021), Theorem 6.1, printed pp.22--25, using their Lemma 3.26: https://arxiv.org/abs/2110.12652. The coordinate repair and its exact retained-marginal accounting are formalized here; the full affine correlation-breaker construction is a separate layer.

theorem Algebraic.Cutwidth.Extractor.smoothMergingSeedWeight_probability {Z : Type u_1} {A : Type u_2} {B : Type u_3} {U : Type u_4} {Q : Type u_5} {V : Type u_6} {Seed : Type u_7} [Fintype Z] [Fintype A] [Fintype B] [Fintype U] [Fintype Q] [Fintype V] [Fintype Seed] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (u : Z → A → U) (q : Z → A → Q) (v : SmoothMergingTranscript Z U Q → B → V) (y : SmoothMergingTranscript Z U Q → B → Seed) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (smoothMergingSeedWeight w l r u q v y)

The actual retained seed law is normalized whenever the original factors are normalized.

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

The output law keeps the actual original right state and all stated left observations.

theorem Algebraic.Cutwidth.Extractor.WeightedStrongSeededExtractor.smooth_two_sided_dist_le {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} {U : Type u_5} {Q : Type u_6} {V : Type u_7} {W : Type u_8} {Seed : Type u_9} {Out : Type u_10} [Fintype Z] [Fintype A] [Fintype B] [Fintype X] [Fintype U] [Fintype Q] [Fintype V] [Fintype W] [Fintype Seed] [Fintype Out] [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) (u : Z → A → U) (q : Z → A → Q) (v : SmoothMergingTranscript Z U Q → B → V) (y : SmoothMergingTranscript Z U Q → B → Seed) (leak : SmoothMergingTranscript Z U Q → V → A → W) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (source : weightDist (observedSeedWeight w l u x) (uniformSecondWeight (observedSeedWeight w l u x)) ≤ ρ) (seed : weightDist (smoothMergingSeedWeight w l r u q v y) (uniformSecondWeight (smoothMergingSeedWeight w l r u q v y)) ≤ δ) : weightDist (smoothTwoSidedExtractionWeight w l r x u q v y leak E) (uniformSecondWeight (smoothTwoSidedExtractionWeight w l r x u q v y leak E)) ≤ ε + δ + ρ + ↑K * ↑(Fintype.card W) * ↑(Fintype.card Q) / ↑(Fintype.card X)

Smooth uniformity before an actual prefix suffices; no conditional source cap is assumed.

theorem Algebraic.Cutwidth.Extractor.smoothMergingSeedWeight_prefix_dist {Z : Type u_1} {A : Type u_2} {B : Type u_3} {U : Type u_4} {Q : Type u_5} {V : Type u_6} {Seed : Type u_7} [Fintype Z] [Fintype A] [Fintype B] [Fintype U] [Fintype Q] [Fintype V] [Fintype Seed] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (u : Z → A → U) (q : Z → A → Q) (v : Z × Q → B → V) (y : Z × Q → B → Seed) (hw : ∀ (z : Z), 0 ≤ w z) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) : weightDist (smoothMergingSeedWeight w l r u q (fun (h : SmoothMergingTranscript Z U Q) => v (h.1.1, h.2)) fun (h : SmoothMergingTranscript Z U Q) => y (h.1.1, h.2)) (uniformSecondWeight (smoothMergingSeedWeight w l r u q (fun (h : SmoothMergingTranscript Z U Q) => v (h.1.1, h.2)) fun (h : SmoothMergingTranscript Z U Q) => y (h.1.1, h.2))) = weightDist (observedSeedWeight (observedTranscriptWeight w l q) (fun (zq : Z × Q) => r zq.1) v y) (uniformSecondWeight (observedSeedWeight (observedTranscriptWeight w l q) (fun (zq : Z × Q) => r zq.1) v y))

Extra original left observations do not change the averaged error of a prefix-only seed.

theorem Algebraic.Cutwidth.Extractor.WeightedStrongSeededExtractor.smooth_two_sided_dist_le_of_prefix_seed {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} {U : Type u_5} {Q : Type u_6} {V : Type u_7} {W : Type u_8} {Seed : Type u_9} {Out : Type u_10} [Fintype Z] [Fintype A] [Fintype B] [Fintype X] [Fintype U] [Fintype Q] [Fintype V] [Fintype W] [Fintype Seed] [Fintype Out] [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) (u : Z → A → U) (q : Z → A → Q) (v : Z × Q → B → V) (y : Z × Q → B → Seed) (leak : SmoothMergingTranscript Z U Q → V → A → W) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (source : weightDist (observedSeedWeight w l u x) (uniformSecondWeight (observedSeedWeight w l u x)) ≤ ρ) (seed : weightDist (observedSeedWeight (observedTranscriptWeight w l q) (fun (zq : Z × Q) => r zq.1) v y) (uniformSecondWeight (observedSeedWeight (observedTranscriptWeight w l q) (fun (zq : Z × Q) => r zq.1) v y)) ≤ δ) : weightDist (smoothTwoSidedExtractionWeight w l r x u q (fun (h : SmoothMergingTranscript Z U Q) => v (h.1.1, h.2)) (fun (h : SmoothMergingTranscript Z U Q) => y (h.1.1, h.2)) leak E) (uniformSecondWeight (smoothTwoSidedExtractionWeight w l r x u q (fun (h : SmoothMergingTranscript Z U Q) => v (h.1.1, h.2)) (fun (h : SmoothMergingTranscript Z U Q) => y (h.1.1, h.2)) leak E)) ≤ ε + δ + ρ + ↑K * ↑(Fintype.card W) * ↑(Fintype.card Q) / ↑(Fintype.card X)

The seed need only be close to uniform with its actual prefix and right observation.