Normalized head and tail disintegration

Positive head rows are normalized by their mass. A zero head row is pointwise zero, so it may use any already normalized positive row as its conditional tail. Normalization of the head guarantees such a row exists.

theorem Algebraic.Cutwidth.Extractor.Internal.blockSource_head_capped {α : Type u_1} [Fintype α] {t K : ℕ} {p : (Fin (t + 1) → α) → ℝ} (source : IsBlockSource p K) : CappedWeight (mapWeight (fun (x : Fin (t + 1) → α) => x 0) p) K

theorem Algebraic.Cutwidth.Extractor.Internal.blockSource_row_caps {α : Type u_1} [Fintype α] {t K : ℕ} {p : (Fin (t + 1) → α) → ℝ} (source : IsBlockSource p K) (a : α) (i : Fin t) (u : Fin (↑i + 1) → α) : ↑K * blockPrefixWeight (fun (z : Fin t → α) => p (Fin.cons a z)) ⋯ u ≤ blockPrefixWeight (fun (z : Fin t → α) => p (Fin.cons a z)) ⋯ (blockPrefix ⋯ u)

theorem Algebraic.Cutwidth.Extractor.Internal.blockSource_tail_of_pos {α : Type u_1} [Fintype α] {t K : ℕ} {p : (Fin (t + 1) → α) → ℝ} (source : IsBlockSource p K) (a : α) (positive : 0 < mapWeight (fun (x : Fin (t + 1) → α) => x 0) p a) : IsBlockSource (fun (z : Fin t → α) => (mapWeight (fun (x : Fin (t + 1) → α) => x 0) p a)⁻¹ * p (Fin.cons a z)) K

theorem Algebraic.Cutwidth.Extractor.Internal.blockSource_exists_head_tail {α : Type u_1} [Fintype α] {t K : ℕ} {p : (Fin (t + 1) → α) → ℝ} (source : IsBlockSource p K) : ∃ (w : α → ℝ) (q : α → (Fin t → α) → ℝ), IsProbabilityWeight w ∧ CappedWeight w K ∧ (∀ (a : α), IsBlockSource (q a) K) ∧ ∀ (a : α) (z : Fin t → α), p (Fin.cons a z) = w a * q a z