Extraction with an arbitrary correlated right state

Specializing two-sided leakage to trivial observations keeps the entire right variable without paying for its alphabet. Projecting away the trivial tags preserves the actual retained marginal. Only the seed's joint distance given the original transcript is charged.

theorem Algebraic.Cutwidth.Extractor.Internal.retainedSeedWeight_observed {Z : Type u_1} {B : Type u_2} {Seed : Type u_3} [Fintype Z] [Fintype B] [Fintype Seed] (w : Z → ℝ) (r : Z → B → ℝ) (y : Z → B → Seed) : observedSeedWeight w r (fun (x : Z) (x_1 : B) => ()) y = mapWeight (fun (zy : Z × Seed) => ((zy.1, ()), zy.2)) (retainedSeedWeight w r y)

theorem Algebraic.Cutwidth.Extractor.Internal.retainedExtractionWeight_project {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} {Seed : Type u_5} {Out : Type u_6} [Fintype Z] [Fintype A] [Fintype B] [Fintype Out] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x : Z → A → X) (y : Z → B → Seed) (E : X → Seed → Out) : mapWeight (fun (p : ((Z × B) × Unit × Unit) × Out) => (p.1.1, p.2)) (twoSidedExtractionWeight w l r x y (fun (x : Z) (x_1 : A) => ()) (fun (x : Z) (x_1 : B) => ()) (fun (x : Z) (x_1 : Unit) (x_2 : A) => ()) E) = retainedExtractionWeight w l r x y E

theorem Algebraic.Cutwidth.Extractor.Internal.retainedExtractionWeight_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} [Fintype Z] [Fintype A] [Fintype B] [Fintype Out] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x : Z → A → X) (y : Z → B → Seed) (E : X → Seed → Out) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (retainedExtractionWeight w l r x y E)

theorem Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededExtractor_retained_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} [Fintype Z] [Fintype A] [Fintype B] [Fintype X] [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) (y : Z → B → Seed) (μ : Z → ℝ) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (nonnegative : ∀ (z : Z), 0 ≤ μ z) (cap : ∀ (z : Z) (x₀ : X), w z * mapWeight (x z) (l z) x₀ ≤ μ z) (seed : weightDist (retainedSeedWeight w r y) (uniformSecondWeight (retainedSeedWeight w r y)) ≤ δ) : weightDist (retainedExtractionWeight w l r x y E) (uniformSecondWeight (retainedExtractionWeight w l r x y E)) ≤ ε + δ + ↑K * ∑ z : Z, μ z

theorem Algebraic.Cutwidth.Extractor.Internal.affineExtractionWeight_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} [Fintype Z] [Fintype A] [Fintype B] [Fintype Out] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x : Z → A → X) (mask : Z → B → X) (y : Z → B → Seed) (combine : X → X → X) (E : X → Seed → Out) (translate : X → Seed → Out ≃ Out) (linear : ∀ (a b : X) (s : Seed), E (combine a b) s = (translate b s) (E a s)) : affineExtractionWeight w l r x mask y combine E = mapWeight (fun (p : (Z × B) × Out) => (p.1, (translate (mask p.1.1 p.1.2) (y p.1.1 p.1.2)) p.2)) (retainedExtractionWeight w l r x y E)

theorem Algebraic.Cutwidth.Extractor.Internal.affineExtractionWeight_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} [Fintype Z] [Fintype A] [Fintype B] [Fintype Out] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x : Z → A → X) (mask : Z → B → X) (y : Z → B → Seed) (combine : X → X → X) (E : X → Seed → Out) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (affineExtractionWeight w l r x mask y combine E)

theorem Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededExtractor_affine_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} [Fintype Z] [Fintype A] [Fintype B] [Fintype X] [Fintype Seed] [Fintype Out] [Nonempty Seed] [Nonempty Out] {E : X → Seed → Out} {K : ℕ} {ε δ : ℝ} (extract : WeightedStrongSeededExtractor E K ε) (error : 0 ≤ ε) (combine : X → X → X) (translate : X → Seed → Out ≃ Out) (linear : ∀ (a b : X) (s : Seed), E (combine a b) s = (translate b s) (E a s)) (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x : Z → A → X) (mask : Z → B → X) (y : Z → B → Seed) (μ : Z → ℝ) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (nonnegative : ∀ (z : Z), 0 ≤ μ z) (cap : ∀ (z : Z) (x₀ : X), w z * mapWeight (x z) (l z) x₀ ≤ μ z) (seed : weightDist (retainedSeedWeight w r y) (uniformSecondWeight (retainedSeedWeight w r y)) ≤ δ) : weightDist (affineExtractionWeight w l r x mask y combine E) (uniformSecondWeight (affineExtractionWeight w l r x mask y combine E)) ≤ ε + δ + ↑K * ∑ z : Z, μ z