English
Version of sum_apply'' with explicit hypotheses for pointwise addition on a FunLike type. If the hypotheses hold, then g.sum k x equals the sum of k i a x over i and a.
Русский
Версия с предположениями для покомпонентного сложения на типе FunLike: сумма равна сумме по i и a.
LaTeX
$$$g.sum k x = g.sum (\lambda i a, k i a x).$$$
Lean4
/-- Version of `Finsupp.sum_apply'` that applies in large generality to linear combinations
of functions in any `FunLike` type on which addition is defined pointwise.
At the time of writing Mathlib does not have a typeclass to express the condition
that addition on a `FunLike` type is pointwise; hence this is asserted via explicit hypotheses. -/
theorem sum_apply'' {A F : Type*} [AddZeroClass A] [AddCommMonoid F] [FunLike F γ B] (g : ι →₀ A) (k : ι → A → F)
(x : γ) (hg0 : ∀ (i : ι), k i 0 = 0) (hgadd : ∀ (i : ι) (a₁ a₂ : A), k i (a₁ + a₂) = k i a₁ + k i a₂)
(h0 : (0 : F) x = 0) (hadd : ∀ (f g : F), (f + g : F) x = f x + g x) : g.sum k x = g.sum (fun i a ↦ k i a x) := by
induction g using Finsupp.induction with
| zero => simp [h0]
| single_add i a f hf ha
ih =>
rw [Finsupp.sum_add_index' hg0 hgadd, Finsupp.sum_add_index', hadd, ih]
· congr 1
rw [Finsupp.sum_single_index (hg0 i), Finsupp.sum_single_index]
simp [hg0, h0]
· simp [hg0, h0]
· simp [hgadd, hadd]
