accumulate_rec — Mathlib

English

There is a simple recurrence: at each internal index i, accumulate equals t(i) plus accumulate at i+1.

Русский

Существует простое рекуррентное соотношение: на каждом внутреннем индексе i accumulate = t(i) + accumulate(i+1).

LaTeX

$$$\\text{accumulate}_{n,m}(t)(i) = t(i) + \\text{accumulate}_{n,m}(t)(i+1)$$$

Lean4

theorem accumulate_rec {i n m : ℕ} (hin : i < n) (him : i + 1 < m) (t : Fin n → ℕ) :
    accumulate n m t ⟨i, Nat.lt_of_succ_lt him⟩ = t ⟨i, hin⟩ + accumulate n m t ⟨i + 1, him⟩ :=
  by
  simp_rw [accumulate_apply]
  convert (add_sum_erase _ _ _).symm
  · ext
    rw [mem_erase]
    simp_rw [mem_filter_univ, i.succ_le_iff, lt_iff_le_and_ne]
    rw [and_comm, ne_comm, ← Fin.val_ne_iff]
  · exact mem_filter.2 ⟨mem_univ _, le_rfl⟩

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