Exact original-law identities around a left prefix observation #
The auxiliary laws expose a single actual prefix. The public smooth law first conditions on its selected old left observation and then uses these identities. Maps of the latent left state preserve all source multiplicities.
theorem
Algebraic.Cutwidth.Extractor.Internal.smooth_factored_map_left
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{C : Type u_4}
[Fintype Z]
[Fintype A]
[Fintype B]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(f : Z → A → C)
:
mapWeight (fun (p : (Z × B) × A) => (p.1, f p.1.1 p.2)) (factoredWeight w l r) = factoredWeight w (fun (z : Z) => mapWeight (f z) (l z)) r
theorem
Algebraic.Cutwidth.Extractor.Internal.smooth_observedSeedWeight_eq_factored
{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]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(v : Z → B → V)
(y : Z → B → Seed)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
:
theorem
Algebraic.Cutwidth.Extractor.Internal.smooth_observed_source_eq_retained
{Z : Type u_1}
{A : Type u_2}
{U : Type u_3}
{X : Type u_4}
[Fintype Z]
[Fintype A]
[Fintype U]
(w : Z → ℝ)
(l : Z → A → ℝ)
(u : Z → A → U)
(x : Z → A → X)
(hl : ∀ (z : Z) (a : A), 0 ≤ l z a)
:
observedSeedWeight w l u x = retainedSeedWeight (observedTranscriptWeight w l u) (observedTranscriptKernel l u) fun (zu : Z × U) => x zu.1
noncomputable def
Algebraic.Cutwidth.Extractor.Internal.smoothPrefixSeedWeight
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{Q : Type u_4}
{V : Type u_5}
{Seed : Type u_6}
[Fintype Z]
[Fintype A]
[Fintype B]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(q : Z → A → Q)
(v : Z × Q → B → V)
(y : Z × Q → B → Seed)
:
The actual right seed after a single original left prefix observation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Algebraic.Cutwidth.Extractor.Internal.smoothPrefixExtractionWeight
{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]
(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)
(E : X → Seed → Out)
:
Actual extraction after a prefix, retaining every unchanged latent right value and left leak.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Algebraic.Cutwidth.Extractor.Internal.smoothPrefixSeedWeight_eq_observed
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{Q : Type u_4}
{V : Type u_5}
{Seed : Type u_6}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype Q]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(q : Z → A → Q)
(v : Z × Q → B → V)
(y : Z × Q → B → Seed)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
:
smoothPrefixSeedWeight w l r q v y = observedSeedWeight (observedTranscriptWeight w l q) (fun (zq : Z × Q) => r zq.1) v y
theorem
Algebraic.Cutwidth.Extractor.Internal.smoothMergingSeedWeight_eq_prefix
{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]
(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)
(hl : ∀ (z : Z) (a : A), 0 ≤ l z a)
:
smoothMergingSeedWeight w l r u q v y = smoothPrefixSeedWeight (observedTranscriptWeight w l u) (observedTranscriptKernel l u) (fun (zu : Z × U) => r zu.1)
(fun (zu : Z × U) => q zu.1) v y
theorem
Algebraic.Cutwidth.Extractor.Internal.smoothTwoSidedExtractionWeight_eq_prefix
{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]
(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)
(hl : ∀ (z : Z) (a : A), 0 ≤ l z a)
:
smoothTwoSidedExtractionWeight w l r x u q v y leak E = smoothPrefixExtractionWeight (observedTranscriptWeight w l u) (observedTranscriptKernel l u)
(fun (zu : Z × U) => r zu.1) (fun (zu : Z × U) => x zu.1) (fun (zu : Z × U) => q zu.1) v y leak E