Two-sided merging after a conditional smooth-source repair #
Repair the honest coordinate while preserving the full original left state. All prefixes, right-seed choices, and retained leaks consequently keep their original joint law. The exact retained marginal makes transfer cost the original distance once. Conditioning first on the selected old left observation gives the public smooth-source consumer.
theorem
Algebraic.Cutwidth.Extractor.Internal.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)
theorem
Algebraic.Cutwidth.Extractor.Internal.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)
theorem
Algebraic.Cutwidth.Extractor.Internal.smoothPrefixExtractionWeight_dist_le
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{X : Type u_4}
{Q : Type u_5}
{V : Type u_6}
{W : Type u_7}
{Seed : Type u_8}
{Out : Type u_9}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype X]
[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)
(q : Z → A → Q)
(v : Z × Q → B → V)
(y : Z × Q → B → Seed)
(leak : Z × Q → V → A → W)
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
(source : weightDist (retainedSeedWeight w l x) (uniformSecondWeight (retainedSeedWeight w l x)) ≤ ρ)
(seed : weightDist (smoothPrefixSeedWeight w l r q v y) (uniformSecondWeight (smoothPrefixSeedWeight w l r q v y)) ≤ δ)
:
weightDist (smoothPrefixExtractionWeight w l r x q v y leak E)
(uniformSecondWeight (smoothPrefixExtractionWeight w l r x q v y leak E)) ≤ ε + δ + ρ + ↑K * ↑(Fintype.card W) * ↑(Fintype.card Q) / ↑(Fintype.card X)
theorem
Algebraic.Cutwidth.Extractor.Internal.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)
theorem
Algebraic.Cutwidth.Extractor.Internal.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)