toNNReal — Mathlib

English

If f has a real-valued sum and certain nonnegativity holds, then the image under Real.toNNReal also has a sum.

Русский

Если f имеет сумму в ℝ и выполняется неотрицательность, то её изображение под Real.toNNReal тоже имеет сумму.

LaTeX

$$HasSum.toNNReal$$

Lean4

protected theorem _root_.HasSum.toNNReal {f : α → ℝ} {y : ℝ} (hf₀ : ∀ n, 0 ≤ f n) (hy : HasSum f y L) :
    HasSum (fun x => Real.toNNReal (f x)) y.toNNReal L :=
  by
  rcases L.neBot_or_eq_bot with _ | hL
  · lift y to ℝ≥0 using hy.nonneg hf₀
    lift f to α → ℝ≥0 using hf₀
    simpa [hasSum_coe] using hy
  · simp [HasSum, hL]

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