English
accumulate(n,m) t is the AddMonoidHom sending t: Fin n → ℕ to a function Fin m → ℕ whose j-th entry is the sum of t_i over all i ≥ j.
Русский
accumulate(n,m) t — линейный гомоморфин, отображающий t: Fin n → ℕ в функцию Fin m → ℕ, где j-я компонента равна сумме t_i по всем i ≥ j.
LaTeX
$$$\\mathrm{accumulate}_{n,m} : (\\mathrm{Fin}\\ n \\to \\mathbb{N}) \\to (\\mathrm{Fin}\\ m \\to \\mathbb{N})$, $(\\mathrm{accumulate}_{n,m} t)(j) = \\sum_{i : \\mathrm{Fin}\n n, j \\le i} t(i)$$$
Lean4
/-- The `j`th entry of `accumulate n m t` is the sum of `t i` over all `i ≥ j`. -/
@[simps]
def accumulate (n m : ℕ) : (Fin n → ℕ) →+ (Fin m → ℕ)
where
toFun t j := ∑ i : Fin n with j.val ≤ i.val, t i
map_zero' := funext <| fun _ ↦ sum_eq_zero <| fun _ _ ↦ rfl
map_add' _ _ := funext <| fun _ ↦ sum_add_distrib
