toNNReal — Mathlib

English

If f: α → R is summable, then the nonnegative part (f(n))^+ is summable as well.

Русский

Если f: α → ℝ является суммируемой, то и сумма положительных частей f (то есть max(f(n),0)) суммируема.

LaTeX

$$$\text{Summable}(f) \implies \text{Summable}\big(n \mapsto \max\{f(n),0\}\big).$$$

Lean4

theorem toNNReal {f : α → ℝ} (hf : Summable f) : Summable fun n => (f n).toNNReal :=
  by
  apply NNReal.summable_coe.1
  refine .of_nonneg_of_le (fun n => NNReal.coe_nonneg _) (fun n => ?_) hf.abs
  simp only [le_abs_self, Real.coe_toNNReal', max_le_iff, abs_nonneg, and_self_iff]

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