Switching the source and seed sides after an observation #
An exact observation update followed by swapping the two sides supplies the conditional product law used by retained extraction. All identities keep the original source variables and include impossible messages.
theorem
Algebraic.Cutwidth.Extractor.Internal.retainedSeedWeight_eq_factored
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{Seed : Type u_4}
[Fintype Z]
[Fintype A]
[Fintype B]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(y : Z → B → Seed)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
:
retainedSeedWeight w r y = mapWeight (fun (p : (Z × B) × A) => (p.1.1, y p.1.1 p.1.2)) (factoredWeight w l r)
theorem
Algebraic.Cutwidth.Extractor.Internal.factoredWeight_observe_swap
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{V : Type u_4}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype V]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(v : Z → B → V)
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
:
mapWeight (fun (p : (Z × B) × A) => (((p.1.1, v p.1.1 p.1.2), p.2), p.1.2)) (factoredWeight w l r) = factoredWeight (observedTranscriptWeight w r v) (observedTranscriptKernel r v) fun (zv : Z × V) => l zv.1
theorem
Algebraic.Cutwidth.Extractor.Internal.alternatingSeedWeight_eq_retained
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{V : Type u_4}
{Seed : Type u_5}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype V]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(v : Z → B → V)
(s : Z × V → A → Seed)
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
:
alternatingSeedWeight w l r v s = retainedSeedWeight (observedTranscriptWeight w r v) (fun (zv : Z × V) => l zv.1) s
theorem
Algebraic.Cutwidth.Extractor.Internal.alternatingExtractionWeight_eq_retained
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{V : Type u_4}
{X : Type u_5}
{Seed : Type u_6}
{Out : Type u_7}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype V]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(v : Z → B → V)
(s : Z × V → A → Seed)
(x : Z → B → X)
(E : X → Seed → Out)
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
:
alternatingExtractionWeight w l r v s x E = retainedExtractionWeight (observedTranscriptWeight w r v) (observedTranscriptKernel r v) (fun (zv : Z × V) => l zv.1)
(fun (zv : Z × V) => x zv.1) s E
theorem
Algebraic.Cutwidth.Extractor.Internal.alternatingExtractionWeight_probability
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{V : Type u_4}
{X : Type u_5}
{Seed : Type u_6}
{Out : Type u_7}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype V]
[Fintype Out]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(v : Z → B → V)
(s : Z × V → A → Seed)
(x : Z → B → X)
(E : X → Seed → Out)
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
:
IsProbabilityWeight (alternatingExtractionWeight w l r v s x E)
theorem
Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededExtractor_alternating_joint_dist_le
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{V : Type u_4}
{X : Type u_5}
{Seed : Type u_6}
{Out : Type u_7}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype V]
[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 → ℝ)
(v : Z → B → V)
(s : Z × V → A → Seed)
(x : Z → B → X)
(μ : Z × V → ℝ)
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
(nonnegative : ∀ (zv : Z × V), 0 ≤ μ zv)
(cap : ∀ (z : Z) (v₀ : V) (x₀ : X), w z * mapWeight (fun (b : B) => (v z b, x z b)) (r z) (v₀, x₀) ≤ μ (z, v₀))
(seed : weightDist (alternatingSeedWeight w l r v s) (uniformSecondWeight (alternatingSeedWeight w l r v s)) ≤ δ)
:
weightDist (alternatingExtractionWeight w l r v s x E)
(uniformSecondWeight (alternatingExtractionWeight w l r v s x E)) ≤ ε + δ + ↑K * ∑ zv : Z × V, μ zv
theorem
Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededExtractor_alternating_dist_le
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{V : Type u_4}
{X : Type u_5}
{Seed : Type u_6}
{Out : Type u_7}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype V]
[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 → ℝ)
(v : Z → B → V)
(s : Z × V → A → Seed)
(x : Z → B → X)
(μ : 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) (r z) x₀ ≤ μ z)
(seed : weightDist (alternatingSeedWeight w l r v s) (uniformSecondWeight (alternatingSeedWeight w l r v s)) ≤ δ)
:
weightDist (alternatingExtractionWeight w l r v s x E)
(uniformSecondWeight (alternatingExtractionWeight w l r v s x E)) ≤ ε + δ + ↑K * ↑(Fintype.card V) * ∑ z : Z, μ z
theorem
Algebraic.Cutwidth.Extractor.Internal.affineAlternatingWeight_eq_alternating
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{X : Type u_4}
{Seed : Type u_5}
{Mid : Type u_6}
{Y : Type u_7}
{Out : Type u_8}
[Fintype Z]
[Fintype A]
[Fintype B]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(x : Z → A → X)
(mask : Z → B → X)
(y : Z → B → Seed)
(source : Z → B → Y)
(combine : X → X → X)
(E : X → Seed → Mid)
(F : Y → Mid → Out)
(translate : Mid → Mid ≃ Mid)
(linear : ∀ (a b : X) (s : Seed), E (combine a b) s = (translate (E b s)) (E a s))
:
affineAlternatingWeight w l r x mask y source combine E F = alternatingExtractionWeight w l r (fun (z : Z) (b : B) => (y z b, E (mask z b) (y z b)))
(fun (zv : Z × Seed × Mid) (a : A) => (translate zv.2.2) (E (x zv.1 a) zv.2.1)) source F
theorem
Algebraic.Cutwidth.Extractor.Internal.affineAlternatingSeed_eq_map
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{X : Type u_4}
{Seed : Type u_5}
{Mid : Type u_6}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype Mid]
(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 → Mid)
(translate : Mid → Mid ≃ Mid)
(linear : ∀ (a b : X) (s : Seed), E (combine a b) s = (translate (E b s)) (E a s))
:
(alternatingSeedWeight w l r (fun (z : Z) (b : B) => (y z b, E (mask z b) (y z b))) fun (zv : Z × Seed × Mid) (a : A) =>
(translate zv.2.2) (E (x zv.1 a) zv.2.1)) = mapWeight (fun (p : (Z × B) × Mid) => ((p.1.1, y p.1.1 p.1.2, E (mask p.1.1 p.1.2) (y p.1.1 p.1.2)), p.2))
(affineExtractionWeight w l r x mask y combine E)
theorem
Algebraic.Cutwidth.Extractor.Internal.affineAlternatingWeight_probability
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{X : Type u_4}
{Seed : Type u_5}
{Mid : Type u_6}
{Y : Type u_7}
{Out : Type u_8}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype Seed]
[Fintype Mid]
[Fintype Out]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(x : Z → A → X)
(mask : Z → B → X)
(y : Z → B → Seed)
(source : Z → B → Y)
(combine : X → X → X)
(E : X → Seed → Mid)
(F : Y → Mid → Out)
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
:
IsProbabilityWeight (affineAlternatingWeight w l r x mask y source combine E F)
theorem
Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededExtractor_affine_alternating_dist_le
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{X : Type u_4}
{Seed : Type u_5}
{Mid : Type u_6}
{Y : Type u_7}
{Out : Type u_8}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype X]
[Fintype Seed]
[Fintype Mid]
[Fintype Y]
[Fintype Out]
[Nonempty Seed]
[Nonempty Mid]
[Nonempty Out]
{E : X → Seed → Mid}
{F : Y → Mid → Out}
{K L : ℕ}
{ε η δ : ℝ}
(first : WeightedStrongSeededExtractor E K ε)
(first_error : 0 ≤ ε)
(second : WeightedStrongSeededExtractor F L η)
(second_error : 0 ≤ η)
(combine : X → X → X)
(translate : Mid → Mid ≃ Mid)
(linear : ∀ (a b : X) (s : Seed), E (combine a b) s = (translate (E 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)
(source : Z → B → Y)
(μ ν : Z → ℝ)
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
(left_nonnegative : ∀ (z : Z), 0 ≤ μ z)
(right_nonnegative : ∀ (z : Z), 0 ≤ ν z)
(left_cap : ∀ (z : Z) (x₀ : X), w z * mapWeight (x z) (l z) x₀ ≤ μ z)
(right_cap : ∀ (z : Z) (y₀ : Y), w z * mapWeight (source z) (r z) y₀ ≤ ν z)
(seed : weightDist (retainedSeedWeight w r y) (uniformSecondWeight (retainedSeedWeight w r y)) ≤ δ)
:
weightDist (affineAlternatingWeight w l r x mask y source combine E F)
(uniformSecondWeight (affineAlternatingWeight w l r x mask y source combine E F)) ≤ η + (ε + δ + ↑K * ∑ z : Z, μ z) + ↑L * ↑(Fintype.card (Seed × Mid)) * ∑ z : Z, ν z