linearCombination_onFinset — Mathlib

English

For s a Finset, f: α → R, g: α → M and hf: ∀ a, f a ≠ 0 → a ∈ s, the linear combination of g with weights onFinset s f hf equals the finite sum over s of f x · g x.

Русский

Для Finset s и функций f, g с условием hf линейная комбинация g со весами на Finset s f hf равна сумме по x∈s f x · g x.

LaTeX

$$$\\operatorname{linearCombination}_R g \\bigl(\\mathrm{onFinset}_R s f hf\\bigr) = \\sum_{x ∈ s} f x \\cdot g x$$$

Lean4

theorem linearCombination_onFinset {s : Finset α} {f : α → R} (g : α → M) (hf : ∀ a, f a ≠ 0 → a ∈ s) :
    linearCombination R g (Finsupp.onFinset s f hf) = Finset.sum s fun x : α => f x • g x := by
  classical
  simp only [linearCombination_apply, Finsupp.sum, Finsupp.onFinset_apply, Finsupp.support_onFinset]
  rw [Finset.sum_filter_of_ne]
  intro x _ h
  contrapose! h
  simp [h]

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