sum_unitVec_mul_slice — Mathlib

English

A holor can be reconstructed from its slices by summing over unit vectors: the sum over i of unitVec d i ⊗ slice x i (proof that i < d) equals x.

Русский

Голор может быть восстановлен из своих срезов: сумма по i из единичных векторов unitVec d i ⊗ slice x i (доказательство i < d) равна x.

LaTeX

$$$$ \\sum_{i=0}^{d-1} \\operatorname{unitVec}(d,i) \\otimes \\operatorname{slice} x i (\\text{proof } i < d) = x $$$$

Lean4

/-- The original holor can be recovered from its slices by multiplying with unit vectors and
summing up. -/
@[simp]
theorem sum_unitVec_mul_slice [Semiring α] (x : Holor α (d :: ds)) :
    (∑ i ∈ (Finset.range d).attach, unitVec d i ⊗ slice x i (Nat.succ_le_of_lt (Finset.mem_range.1 i.prop))) = x :=
  by
  apply slice_eq _ _ _
  ext i hid
  rw [← slice_sum]
  simp only [slice_unitVec_mul hid]
  rw [Finset.sum_eq_single (Subtype.mk i <| Finset.mem_range.2 hid)]
  · simp
  · intro (b : { x // x ∈ Finset.range d }) (_ : b ∈ (Finset.range d).attach) (hbi : b ≠ ⟨i, _⟩)
    have hbi' : i ≠ b := by simpa only [Ne, Subtype.ext_iff, Subtype.coe_mk] using hbi.symm
    simp [hbi']
  · intro (hid' : Subtype.mk i _ ∉ Finset.attach (Finset.range d))
    exfalso
    exact absurd (Finset.mem_attach _ _) hid'

Похожие утверждения