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.

Notation #

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

source

noncomputable instance NNReal.instFloorSemiring :

FloorSemiring NNReal

Equations

source

@[simp]

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

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

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

@[simp]

theorem NNReal.coe_mulSingle {α : Type u_1} [DecidableEq α] (a : α) (b : NNReal) (c : α) :

↑(Pi.mulSingle a b c) = Pi.mulSingle a (↑b) c

source

@[simp]

theorem NNReal.coe_single {α : Type u_1} [DecidableEq α] (a : α) (b : NNReal) (c : α) :

↑(Pi.single a b c) = Pi.single a (↑b) c

source

theorem NNReal.coe_list_sum (l : List NNReal) :

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

source

theorem NNReal.coe_list_prod (l : List NNReal) :

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

source

theorem NNReal.coe_multiset_sum (s : Multiset NNReal) :

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

source

theorem NNReal.coe_multiset_prod (s : Multiset NNReal) :

↑s.prod = (Multiset.map 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

source

@[simp]

theorem NNReal.bddAbove_natCast_image_iff {s : Set ℕ} :

BddAbove (Nat.cast '' s) ↔ BddAbove s

source

@[simp]

theorem NNReal.bddAbove_range_natCast_iff {ι : Sort u_2} (f : ι → ℕ) :

BddAbove (Set.range fun (x : ι) => ↑(f x)) ↔ BddAbove (Set.range f)

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.lean. See also mul_tsub and tsub_mul.

source

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