coeff_hsum_eq_sum_of_subset — Mathlib

English

If the set of indices where a given coefficient is nonzero is contained in a finite set t, then the hsum coefficient equals the finite sum over t.

Русский

Если множество индексов, где коэффициент не равен нулю, содержится в конечном множестве t, то коэффициент суммы по Хану равен сумме по t.

LaTeX

$$$\\big(\\{a\\mid (s a).coeff g \\neq 0\\} \\subseteq t\\big) \\Rightarrow s.hsum.coeff g = \\sum_{i\\in t} (s i).coeff g$$$

Lean4

theorem coeff_hsum_eq_sum_of_subset {s : SummableFamily Γ R α} {g : Γ} {t : Finset α}
    (h : {a | (s a).coeff g ≠ 0} ⊆ t) : s.hsum.coeff g = ∑ i ∈ t, (s i).coeff g :=
  by
  simp only [coeff_hsum, finsum_eq_sum _ (s.finite_co_support _)]
  exact sum_subset (Set.Finite.toFinset_subset.mpr h) (by simp)

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