Prepending a capped head to mixtures of block-source tails

The prefix inequalities are homogeneous in each head row. Nonnegative coefficients with prescribed row totals therefore preserve the tail caps, without normalizing any zero-mass row.

theorem Algebraic.Cutwidth.Extractor.Internal.blockSource_of_row_caps {α : Type u_1} [Fintype α] {t K : ℕ} (p : (Fin (t + 1) → α) → ℝ) (probability : IsProbabilityWeight p) (head_cap : CappedWeight (mapWeight (fun (x : Fin (t + 1) → α) => x 0) p) K) (row_caps : ∀ (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)) : IsBlockSource p K

theorem Algebraic.Cutwidth.Extractor.Internal.blockSource_of_prepend_mixture {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] {t K : ℕ} (r : (Fin (t + 1) → α) → ℝ) (target : α → ℝ) (tail : ι → (Fin t → α) → ℝ) (c : α → ι → ℝ) (target_prob : IsProbabilityWeight target) (target_cap : CappedWeight target K) (tail_source : ∀ (a : ι), IsBlockSource (tail a) K) (coeff_nonneg : ∀ (h : α) (a : ι), 0 ≤ c h a) (rows : ∀ (h : α), ∑ a : ι, c h a = target h) (factor : ∀ (h : α) (z : Fin t → α), r (Fin.cons h z) = ∑ a : ι, c h a * tail a z) : IsBlockSource r K

theorem Algebraic.Cutwidth.Extractor.Internal.blockSource_prepend {α : Type u_1} [Fintype α] {t K : ℕ} (w : α → ℝ) (tail : α → (Fin t → α) → ℝ) (head_prob : IsProbabilityWeight w) (head_cap : CappedWeight w K) (tail_source : ∀ (a : α), IsBlockSource (tail a) K) : IsBlockSource (fun (x : Fin (t + 1) → α) => w (x 0) * tail (x 0) (Fin.tail x)) K