+# Transport for the multiblock splitting induction

A head/tail factorization identifies both the head marginal and the joint weight. Splitting such a joint law splits the conditional tails and prepends the two head coordinates. Equality of tuple lengths preserves block sources.

theorem Algebraic.Cutwidth.Extractor.Internal.splitBlock_source_cast {α : Type u_1} [Fintype α] {n m K : ℕ} (h : n = m) (p : (Fin m → α) → ℝ) (source : IsBlockSource p K) : IsBlockSource (mapWeight (fun (x : Fin m → α) (i : Fin n) => x (Fin.cast h i)) p) K

theorem Algebraic.Cutwidth.Extractor.Internal.splitBlock_head_eq {α : Type u_1} [Fintype α] {t : ℕ} (p : (Fin (t + 1) → α) → ℝ) (w : α → ℝ) (tail : α → (Fin t → α) → ℝ) (probability : ∀ (a : α), IsProbabilityWeight (tail a)) (factor : ∀ (a : α) (z : Fin t → α), p (Fin.cons a z) = w a * tail a z) : mapWeight (fun (x : Fin (t + 1) → α) => x 0) p = w

theorem Algebraic.Cutwidth.Extractor.Internal.splitBlock_mapWeight_of_factor {α : Type u_1} [Fintype α] {t : ℕ} (p : (Fin (t + 1) → α) → ℝ) (w : α → ℝ) (tail : α → (Fin t → α) → ℝ) (factor : ∀ (a : α) (z : Fin t → α), p (Fin.cons a z) = w a * tail a z) : (mapWeight (fun (az : α × (Fin t → α)) => Fin.cons az.1 az.2) fun (az : α × (Fin t → α)) => w az.1 * tail az.1 az.2) = p

theorem Algebraic.Cutwidth.Extractor.Internal.splitBlock_map_of_factor {α : Type u_1} [Fintype α] {t : ℕ} (p : (Fin (t + 1) → α × α) → ℝ) (w : α × α → ℝ) (tail : α × α → (Fin t → α × α) → ℝ) (factor : ∀ (a : α × α) (z : Fin t → α × α), p (Fin.cons a z) = w a * tail a z) : mapWeight (⇑(splitBlockEquiv α (t + 1))) p = mapWeight (fun (x : Fin (2 * t + 2) → α) (i : Fin (2 * t.succ)) => x (Fin.cast ⋯ i)) (mapWeight ⇑(pairPrependEquiv α (2 * t)) fun (az : (α × α) × (Fin (2 * t) → α)) => w az.1 * mapWeight (⇑(splitBlockEquiv α t)) (tail az.1) az.2)