Basic results on nonnegative real numbers #

This file contains all results on NNReal that do not directly follow from its basic structure. As a consequence, it is a bit of a random collection of results, and is a good target for cleanup.

Notations #

This file uses ℝ≥0 as a localized notation for NNReal.

source

noncomputable instance NNReal.instFloorSemiring :

FloorSemiring NNReal

Equations

NNReal.instFloorSemiring = Nonneg.floorSemiring

source

@[simp]

theorem NNReal.coe_indicator {α : Type u_1} (s : Set α) (f : α → NNReal) (a : α) :

↑(s.indicator f a) = s.indicator (fun (x : α) => ↑(f x)) a

source

theorem NNReal.coe_list_sum (l : List NNReal) :

↑l.sum = (List.map NNReal.toReal l).sum

source

theorem NNReal.coe_list_prod (l : List NNReal) :

↑l.prod = (List.map NNReal.toReal l).prod

source

theorem NNReal.coe_multiset_sum (s : Multiset NNReal) :

↑s.sum = (Multiset.map NNReal.toReal s).sum

source

theorem NNReal.coe_multiset_prod (s : Multiset NNReal) :

↑s.prod = (Multiset.map NNReal.toReal s).prod

source

@[simp]

theorem NNReal.coe_sum {ι : Type u_1} (s : Finset ι) (f : ι → NNReal) :

↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)

source

@[simp]

theorem NNReal.coe_expect {ι : Type u_1} (s : Finset ι) (f : ι → NNReal) :

↑(s.expect fun (i : ι) => f i) = s.expect fun (i : ι) => ↑(f i)

source

theorem Real.toNNReal_sum_of_nonneg {ι : Type u_1} {s : Finset ι} {f : ι → ℝ} (hf : ∀ i ∈ s, 0 ≤ f i) :

(∑ a ∈ s, f a).toNNReal = ∑ a ∈ s, (f a).toNNReal

source

@[simp]

theorem NNReal.coe_prod {ι : Type u_1} (s : Finset ι) (f : ι → NNReal) :

↑(∏ a ∈ s, f a) = ∏ a ∈ s, ↑(f a)

source

theorem Real.toNNReal_prod_of_nonneg {ι : Type u_1} {s : Finset ι} {f : ι → ℝ} (hf : ∀ a ∈ s, 0 ≤ f a) :

(∏ a ∈ s, f a).toNNReal = ∏ a ∈ s, (f a).toNNReal

source

theorem NNReal.le_iInf_add_iInf {ι : Sort u_2} {ι' : Sort u_3} [Nonempty ι] [Nonempty ι'] {f : ι → NNReal} {g : ι' → NNReal} {a : NNReal} (h : ∀ (i : ι) (j : ι'), a ≤ f i + g j) :

a ≤ (⨅ (i : ι), f i) + ⨅ (j : ι'), g j

source

theorem NNReal.mul_finset_sup {α : Type u_2} (r : NNReal) (s : Finset α) (f : α → NNReal) :

r * s.sup f = s.sup fun (a : α) => r * f a

source

theorem NNReal.finset_sup_mul {α : Type u_2} (s : Finset α) (f : α → NNReal) (r : NNReal) :

s.sup f * r = s.sup fun (a : α) => f a * r

source

theorem NNReal.finset_sup_div {α : Type u_2} {f : α → NNReal} {s : Finset α} (r : NNReal) :

s.sup f / r = s.sup fun (a : α) => f a / r

Lemmas about subtraction #

In this section we provide a few lemmas about subtraction that do not fit well into any other typeclass. For lemmas about subtraction and addition see lemmas about OrderedSub in the file Mathlib.Algebra.Order.Sub.Basic. See also mul_tsub and tsub_mul.

source

theorem NNReal.sub_div (a b c : NNReal) :