tsum_mul_left — Mathlib

English

For a fixed a ∈ ENNReal and f : α → ENNReal, ∑' i, a * f(i) = a * ∑' i, f(i).

Русский

Для фиксированного a и функции f: α → ENNReal сумма слева от умножения равна умножению на сумму: ∑' i, a·f(i) = a·∑' i, f(i).

LaTeX

$$$\sum'_{i \in \alpha} a \cdot f(i) = a \cdot \sum'_{i \in \alpha} f(i)$$$

Lean4

protected theorem tsum_mul_left : ∑' i, a * f i = a * ∑' i, f i :=
  by
  by_cases hf : ∀ i, f i = 0
  · simp [hf]
  · rw [← ENNReal.tsum_eq_zero] at hf
    have : Tendsto (fun s : Finset α => ∑ j ∈ s, a * f j) atTop (𝓝 (a * ∑' i, f i)) :=
      by
      simp only [← Finset.mul_sum]
      exact ENNReal.Tendsto.const_mul ENNReal.summable.hasSum (Or.inl hf)
    exact HasSum.tsum_eq this

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