Exact finite factorization after an observation

Multiplying an observation's marginal by its conditional row recovers the original mass, including null rows. Deterministic maps retaining both original side variables therefore give exact factored laws on the extended transcript. Alternating observations compose these equalities.

theorem Algebraic.Cutwidth.Extractor.Internal.transcript_map_graph {A : Type u_1} {U : Type u_2} [Fintype A] (p : A → ℝ) (f : A → U) (u : U) (a : A) : mapWeight (fun (a : A) => (f a, a)) p (u, a) = if f a = u then p a else 0

theorem Algebraic.Cutwidth.Extractor.Internal.transcript_graph_first {A : Type u_1} {U : Type u_2} [Fintype A] (p : A → ℝ) (f : A → U) : firstWeight (mapWeight (fun (a : A) => (f a, a)) p) = mapWeight f p

theorem Algebraic.Cutwidth.Extractor.Internal.observedTranscriptKernel_factor {Z : Type u_1} {A : Type u_2} {U : Type u_3} [Fintype A] (p : Z → A → ℝ) (f : Z → A → U) (nonnegative : ∀ (z : Z) (a : A), 0 ≤ p z a) (zu : Z × U) (a : A) : mapWeight (f zu.1) (p zu.1) zu.2 * observedTranscriptKernel p f zu a = if f zu.1 a = zu.2 then p zu.1 a else 0

theorem Algebraic.Cutwidth.Extractor.Internal.observedTranscriptKernel_probability {Z : Type u_1} {A : Type u_2} {U : Type u_3} [Fintype A] [Fintype U] (p : Z → A → ℝ) (f : Z → A → U) (probability : ∀ (z : Z), IsProbabilityWeight (p z)) (zu : Z × U) : IsProbabilityWeight (observedTranscriptKernel p f zu)

theorem Algebraic.Cutwidth.Extractor.Internal.observedTranscriptWeight_mul_kernel {Z : Type u_1} {A : Type u_2} {U : Type u_3} [Fintype A] (w : Z → ℝ) (p : Z → A → ℝ) (f : Z → A → U) (nonnegative : ∀ (z : Z) (a : A), 0 ≤ p z a) (zu : Z × U) (a : A) : observedTranscriptWeight w p f zu * observedTranscriptKernel p f zu a = if f zu.1 a = zu.2 then w zu.1 * p zu.1 a else 0

theorem Algebraic.Cutwidth.Extractor.Internal.observedTranscriptKernel_eq_uniform {Z : Type u_1} {A : Type u_2} {U : Type u_3} [Fintype A] (p : Z → A → ℝ) (f : Z → A → U) (zu : Z × U) (zero : mapWeight (f zu.1) (p zu.1) zu.2 = 0) : observedTranscriptKernel p f zu = uniformWeight A

theorem Algebraic.Cutwidth.Extractor.Internal.observedTranscriptWeight_probability {Z : Type u_1} {A : Type u_2} {U : Type u_3} [Fintype Z] [Fintype A] [Fintype U] (w : Z → ℝ) (p : Z → A → ℝ) (f : Z → A → U) (hw : IsProbabilityWeight w) (hp : ∀ (z : Z), IsProbabilityWeight (p z)) : IsProbabilityWeight (observedTranscriptWeight w p f)

theorem Algebraic.Cutwidth.Extractor.Internal.factoredWeight_probability {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (factoredWeight w l r)

theorem Algebraic.Cutwidth.Extractor.Internal.factoredWeight_observe_left {Z : Type u_1} {A : Type u_2} {B : Type u_3} {U : Type u_4} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (f : Z → A → U) (nonnegative : ∀ (z : Z) (a : A), 0 ≤ l z a) : mapWeight (fun (p : (Z × B) × A) => (((p.1.1, f p.1.1 p.2), p.1.2), p.2)) (factoredWeight w l r) = factoredWeight (observedTranscriptWeight w l f) (observedTranscriptKernel l f) fun (zu : Z × U) => r zu.1

theorem Algebraic.Cutwidth.Extractor.Internal.factoredWeight_observe_right {Z : Type u_1} {A : Type u_2} {B : Type u_3} {V : Type u_4} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (g : Z → B → V) (nonnegative : ∀ (z : Z) (b : B), 0 ≤ r z b) : mapWeight (fun (p : (Z × B) × A) => (((p.1.1, g p.1.1 p.1.2), p.1.2), p.2)) (factoredWeight w l r) = factoredWeight (observedTranscriptWeight w r g) (fun (zv : Z × V) => l zv.1) (observedTranscriptKernel r g)

theorem Algebraic.Cutwidth.Extractor.Internal.factoredWeight_observe_left_right {Z : Type u_1} {A : Type u_2} {B : Type u_3} {U : Type u_4} {V : Type u_5} [Fintype Z] [Fintype A] [Fintype B] [Fintype U] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (f : Z → A → U) (g : Z × U → B → V) (left_nonnegative : ∀ (z : Z) (a : A), 0 ≤ l z a) (right_nonnegative : ∀ (z : Z) (b : B), 0 ≤ r z b) : mapWeight (fun (p : (Z × B) × A) => ((((p.1.1, f p.1.1 p.2), g (p.1.1, f p.1.1 p.2) p.1.2), p.1.2), p.2)) (factoredWeight w l r) = factoredWeight (observedTranscriptWeight (observedTranscriptWeight w l f) (fun (zu : Z × U) => r zu.1) g) (fun (zuv : (Z × U) × V) => observedTranscriptKernel l f zuv.1) (observedTranscriptKernel (fun (zu : Z × U) => r zu.1) g)

theorem Algebraic.Cutwidth.Extractor.Internal.observedTranscript_left_right_probability {Z : Type u_1} {A : Type u_2} {B : Type u_3} {U : Type u_4} {V : Type u_5} [Fintype Z] [Fintype A] [Fintype B] [Fintype U] [Fintype V] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (f : Z → A → U) (g : Z × U → B → V) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (observedTranscriptWeight (observedTranscriptWeight w l f) (fun (zu : Z × U) => r zu.1) g) ∧ (∀ (zuv : (Z × U) × V), IsProbabilityWeight (observedTranscriptKernel l f zuv.1)) ∧ ∀ (zuv : (Z × U) × V), IsProbabilityWeight (observedTranscriptKernel (fun (zu : Z × U) => r zu.1) g zuv)