sigma_sum — Mathlib

English

The total sum of a function over a sigma-typed finsupp equals the iterated sum over its split components.

Русский

Общая сумма функции над зависимой суммой равна повторному суммированию по разбиениям компонент.

LaTeX

$$$l.\\\\sum f = \\\\sum_{i \\\\in splitSupport(l)} (l.\\\\split i).\\\\sum(\\\\lambda a b \\,=>\\, f\\\\langle i,a\\\\rangle b)$$$

Lean4

theorem sigma_sum [AddCommMonoid N] (f : (Σ i : ι, αs i) → M → N) :
    l.sum f = ∑ i ∈ splitSupport l, (split l i).sum fun (a : αs i) b => f ⟨i, a⟩ b := by
  simp only [sum, sigma_support, sum_sigma, split_apply]

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