Attaching an unchanged conditional tail to a repaired head

Attaching the same normalized tail law to two head/latent-state laws preserves their total variation exactly. Prepending the head then forgets only the latent state. The coordinate formulas retain every source occurrence and apply also to zero-mass rows.

theorem Algebraic.Cutwidth.Extractor.Internal.attachTail_probability {α : Type u_1} {Ω : Type u_2} {β : Type u_3} [Fintype α] [Fintype Ω] [Fintype β] (c : Ω × α → ℝ) (tail : α → β → ℝ) (hc : IsProbabilityWeight c) (htail : ∀ (a : α), IsProbabilityWeight (tail a)) : IsProbabilityWeight fun (z : (Ω × α) × β) => c z.1 * tail z.1.2 z.2

theorem Algebraic.Cutwidth.Extractor.Internal.attachTail_dist {α : Type u_1} {Ω : Type u_2} {β : Type u_3} [Fintype α] [Fintype Ω] [Fintype β] (c d : Ω × α → ℝ) (tail : α → β → ℝ) (htail : ∀ (a : α), IsProbabilityWeight (tail a)) : (weightDist (fun (z : (Ω × α) × β) => c z.1 * tail z.1.2 z.2) fun (z : (Ω × α) × β) => d z.1 * tail z.1.2 z.2) = weightDist c d

theorem Algebraic.Cutwidth.Extractor.Internal.attachTail_fst {α : Type u_1} {Ω : Type u_2} {β : Type u_3} [Fintype α] [Fintype Ω] [Fintype β] (c : Ω × α → ℝ) (tail : α → β → ℝ) (htail : ∀ (a : α), IsProbabilityWeight (tail a)) : (mapWeight Prod.fst fun (z : (Ω × α) × β) => c z.1 * tail z.1.2 z.2) = c

theorem Algebraic.Cutwidth.Extractor.Internal.prependWeight_apply {α : Type u_1} {Ω : Type u_2} [Fintype α] [Fintype Ω] {t : ℕ} (c : Ω × α → ℝ) (tail : α → (Fin t → Ω) → ℝ) (h : Ω) (z : Fin t → Ω) : mapWeight (fun (az : (Ω × α) × (Fin t → Ω)) => Fin.cons az.1.1 az.2) (fun (az : (Ω × α) × (Fin t → Ω)) => c az.1 * tail az.1.2 az.2) (Fin.cons h z) = ∑ a : α, c (h, a) * tail a z

theorem Algebraic.Cutwidth.Extractor.Internal.prependWeight_head {α : Type u_1} {Ω : Type u_2} [Fintype α] [Fintype Ω] {t : ℕ} (c : Ω × α → ℝ) (tail : α → (Fin t → Ω) → ℝ) (htail : ∀ (a : α), IsProbabilityWeight (tail a)) : mapWeight (fun (z : Fin (t + 1) → Ω) => z 0) (mapWeight (fun (az : (Ω × α) × (Fin t → Ω)) => Fin.cons az.1.1 az.2) fun (az : (Ω × α) × (Fin t → Ω)) => c az.1 * tail az.1.2 az.2) = firstWeight c

theorem Algebraic.Cutwidth.Extractor.Internal.prependWeight_deterministic {α : Type u_1} {Ω : Type u_2} [Fintype α] [Fintype Ω] {t : ℕ} (w : α → ℝ) (tail : α → (Fin t → Ω) → ℝ) (f : α → Ω) : (mapWeight (fun (az : (Ω × α) × (Fin t → Ω)) => Fin.cons az.1.1 az.2) fun (az : (Ω × α) × (Fin t → Ω)) => mapWeight (fun (a : α) => (f a, a)) w az.1 * tail az.1.2 az.2) = mapWeight (fun (az : α × (Fin t → Ω)) => Fin.cons (f az.1) az.2) fun (az : α × (Fin t → Ω)) => w az.1 * tail az.1 az.2