Head and prefix weight identities

Separating the head from a finite tuple reindexes a sum bijectively. A nonempty prefix fixes the head and then takes the corresponding prefix of the unnormalized tail row. These identities hold for arbitrary weights.

theorem Algebraic.Cutwidth.Extractor.Internal.block_sum_cons {α : Type u_1} [Fintype α] {t : ℕ} (p : (Fin (t + 1) → α) → ℝ) : ∑ x : Fin (t + 1) → α, p x = ∑ a : α, ∑ z : Fin t → α, p (Fin.cons a z)

theorem Algebraic.Cutwidth.Extractor.Internal.blockPrefix_cons {α : Type u_1} {i t : ℕ} (h : i ≤ t) (a : α) (z : Fin t → α) : blockPrefix ⋯ (Fin.cons a z) = Fin.cons a (blockPrefix h z)

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

theorem Algebraic.Cutwidth.Extractor.Internal.blockPrefixWeight_scale {α : Type u_1} [Fintype α] {i t : ℕ} (p : (Fin t → α) → ℝ) (c : ℝ) (h : i ≤ t) (u : Fin i → α) : blockPrefixWeight (fun (x : Fin t → α) => c * p x) h u = c * blockPrefixWeight p h u

theorem Algebraic.Cutwidth.Extractor.Internal.mapWeight_blockHead_apply {α : Type u_1} [Fintype α] {t : ℕ} (p : (Fin (t + 1) → α) → ℝ) (a : α) : mapWeight (fun (x : Fin (t + 1) → α) => x 0) p a = ∑ z : Fin t → α, p (Fin.cons a z)