toNNReal_sum_of_nonneg — Mathlib

English

Real.toNNReal distributes over finite sums of nonnegative functions: Real.toNNReal (sum f) = sum Real.toNNReal (f).

Русский

Real.toNNReal распределяет по суммам над неотрицательными функциями: Real.toNNReal(\\\\sum f) = \\\\sum Real.toNNReal(f).

LaTeX

$$$\\\\text{Real.toNNReal}(\\\\sum a \\\\in s, f a) = \\\\sum a \\\\in s, \\text{Real.toNNReal}(f a) \\; (\\\\text{при } f a \\ge 0).$$$

Lean4

theorem _root_.Real.toNNReal_sum_of_nonneg (hf : ∀ i ∈ s, 0 ≤ f i) :
    Real.toNNReal (∑ a ∈ s, f a) = ∑ a ∈ s, Real.toNNReal (f a) :=
  by
  rw [← coe_inj, NNReal.coe_sum, Real.coe_toNNReal _ (Finset.sum_nonneg hf)]
  exact Finset.sum_congr rfl fun x hxs => by rw [Real.coe_toNNReal _ (hf x hxs)]

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