Module docstring
{"# Finsupp.sum and Finsupp.prod over Fin
This file contains theorems relevant to big operators in finitely supported functions over Fin.
"}
Finsupp.sum_cons
theorem
[AddCommMonoid M] (n : ℕ) (σ : Fin n →₀ M) (i : M) : (sum (cons i σ) fun _ e ↦ e) = i + sum σ (fun _ e ↦ e)
Full source
lemma sum_cons [AddCommMonoid M] (n : ℕ) (σ : FinFin n →₀ M) (i : M) :
(sum (cons i σ) fun _ e ↦ e) = i + sum σ (fun _ e ↦ e) := by
rw [sum_fintype _ _ (fun _ => rfl), sum_fintype _ _ (fun _ => rfl)]
exact Fin.sum_cons i σInformal description
Let $M$ be an additive commutative monoid. For any natural number $n$, a finitely supported function $\sigma \colon \mathrm{Fin}\,n \to M$, and an element $i \in M$, the sum of the values of the finitely supported function $\mathrm{cons}\,i\,\sigma \colon \mathrm{Fin}\,(n+1) \to M$ is equal to $i$ plus the sum of the values of $\sigma$. That is,
\[
\sum_{x \in \mathrm{Fin}\,(n+1)} (\mathrm{cons}\,i\,\sigma)(x) = i + \sum_{x \in \mathrm{Fin}\,n} \sigma(x).
\]
Finsupp.sum_cons'
theorem
[Zero M] [AddCommMonoid N] (n : ℕ) (σ : Fin n →₀ M) (i : M) (f : Fin (n + 1) → M → N) (h : ∀ x, f x 0 = 0) :
(sum (Finsupp.cons i σ) f) = f 0 i + sum σ (Fin.tail f)
Full source
lemma sum_cons' [Zero M] [AddCommMonoid N] (n : ℕ) (σ : FinFin n →₀ M) (i : M)
(f : Fin (n+1) → M → N) (h : ∀ x, f x 0 = 0) :
(sum (Finsupp.cons i σ) f) = f 0 i + sum σ (Fin.tail f) := by
rw [sum_fintype _ _ (fun _ => by apply h), sum_fintype _ _ (fun _ => by apply h)]
simp_rw [Fin.sum_univ_succ, cons_zero, cons_succ]
congrInformal description
Let $M$ be a type with a zero element and $N$ be an additive commutative monoid. For any natural number $n$, a finitely supported function $\sigma \colon \mathrm{Fin}\,n \to₀ M$, an element $i \in M$, and a function $f \colon \mathrm{Fin}\,(n+1) \to M \to N$ such that $f\,x\,0 = 0$ for all $x$, the sum over the finitely supported function $\mathrm{cons}\,i\,\sigma$ satisfies
\[
\sum_{x \in \mathrm{Fin}\,(n+1)} f\,x\,(\mathrm{cons}\,i\,\sigma\,x) = f\,0\,i + \sum_{x \in \mathrm{Fin}\,n} (\mathrm{tail}\,f)\,x\,\sigma\,x.
\]