English
For any f : ι →₀ α, i ∈ ι, a ∈ α and g : ι → α → β with suitable linearity, the usual distributive-like identity holds: (f.update i a).sum g + g i (f i) = f.sum g + g i a.
Русский
Для любой f : ι →₀ α, i ∈ ι, a ∈ α и g : ι → α → β при соблюдении линейности выполняется тождество: (f.update i a).sum g + g i (f i) = f.sum g + g i a.
LaTeX
$$$$ (f.update i a).sum g + g i (f i) = f.sum g + g i a. $$$$
Lean4
theorem sum_update_add [AddZeroClass α] [AddCommMonoid β] (f : ι →₀ α) (i : ι) (a : α) (g : ι → α → β)
(hg : ∀ i, g i 0 = 0) (hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂) :
(f.update i a).sum g + g i (f i) = f.sum g + g i a :=
by
rw [update_eq_erase_add_single, sum_add_index' hg hgg]
conv_rhs => rw [← Finsupp.update_self f i]
rw [update_eq_erase_add_single, sum_add_index' hg hgg, add_assoc, add_assoc]
congr 1
rw [add_comm, sum_single_index (hg _), sum_single_index (hg _)]
