# Documentation

Mathlib.Data.Real.NNReal

# Nonnegative real numbers #

In this file we define NNReal (notation: ℝ≥0) to be the type of non-negative real numbers, a.k.a. the interval [0, ∞). We also define the following operations and structures on ℝ≥0:

• the order on ℝ≥0 is the restriction of the order on ℝ; these relations define a conditionally complete linear order with a bottom element, ConditionallyCompleteLinearOrderBot;

• a + b and a * b are the restrictions of addition and multiplication of real numbers to ℝ≥0; these operations together with 0 = ⟨0, _⟩ and 1 = ⟨1, _⟩ turn ℝ≥0 into a conditionally complete linear ordered archimedean commutative semifield; we have no typeclass for this in mathlib yet, so we define the following instances instead:

• LinearOrderedSemiring ℝ≥0;
• OrderedCommSemiring ℝ≥0;
• CanonicallyOrderedCommSemiring ℝ≥0;
• LinearOrderedCommGroupWithZero ℝ≥0;
• CanonicallyLinearOrderedAddMonoid ℝ≥0;
• Archimedean ℝ≥0;
• ConditionallyCompleteLinearOrderBot ℝ≥0.

These instances are derived from corresponding instances about the type {x : α // 0 ≤ x} in an appropriate ordered field/ring/group/monoid α, see Mathlib.Algebra.Order.Nonneg.Ring.

• Real.toNNReal x is defined as ⟨max x 0, _⟩, i.e. ↑(Real.toNNReal x) = x when 0 ≤ x and ↑(Real.toNNReal x) = 0 otherwise.

We also define an instance CanLift ℝ ℝ≥0. This instance can be used by the lift tactic to replace x : ℝ and hx : 0 ≤ x in the proof context with x : ℝ≥0 while replacing all occurrences of x with ↑x. This tactic also works for a function f : α → ℝ with a hypothesis hf : ∀ x, 0 ≤ f x.

## Notations #

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

Nonnegative real numbers.

Instances For
Instances For
noncomputable instance NNReal.instSubNNReal :

Coercion ℝ≥0 → ℝ.

Instances For
@[simp]
theorem NNReal.val_eq_coe (n : NNReal) :
n = n
theorem NNReal.eq {n : NNReal} {m : NNReal} :
n = mn = m
theorem NNReal.eq_iff {n : NNReal} {m : NNReal} :
n = m n = m
theorem NNReal.ne_iff {x : NNReal} {y : NNReal} :
x y x y
theorem NNReal.forall {p : } :
((x : NNReal) → p x) (x : ) → (hx : 0 x) → p { val := x, property := hx }
theorem NNReal.exists {p : } :
(x, p x) x hx, p { val := x, property := hx }
noncomputable def Real.toNNReal (r : ) :

Reinterpret a real number r as a non-negative real number. Returns 0 if r < 0.

Instances For
theorem Real.coe_toNNReal (r : ) (hr : 0 r) :
↑() = r
theorem Real.toNNReal_of_nonneg {r : } (hr : 0 r) :
= { val := r, property := hr }
theorem Real.le_coe_toNNReal (r : ) :
r ↑()
theorem NNReal.coe_nonneg (r : NNReal) :
0 r
@[simp]
theorem NNReal.coe_mk (a : ) (ha : 0 a) :
{ val := a, property := ha } = a
@[simp]
theorem NNReal.coe_eq {r₁ : NNReal} {r₂ : NNReal} :
r₁ = r₂ r₁ = r₂
@[simp]
theorem NNReal.coe_zero :
0 = 0
@[simp]
theorem NNReal.coe_one :
1 = 1
@[simp]
theorem NNReal.coe_add (r₁ : NNReal) (r₂ : NNReal) :
↑(r₁ + r₂) = r₁ + r₂
@[simp]
theorem NNReal.coe_mul (r₁ : NNReal) (r₂ : NNReal) :
↑(r₁ * r₂) = r₁ * r₂
@[simp]
theorem NNReal.coe_inv (r : NNReal) :
r⁻¹ = (r)⁻¹
@[simp]
theorem NNReal.coe_div (r₁ : NNReal) (r₂ : NNReal) :
↑(r₁ / r₂) = r₁ / r₂
theorem NNReal.coe_two :
2 = 2
@[simp]
theorem NNReal.coe_sub {r₁ : NNReal} {r₂ : NNReal} (h : r₂ r₁) :
↑(r₁ - r₂) = r₁ - r₂
@[simp]
theorem NNReal.coe_eq_zero (r : NNReal) :
r = 0 r = 0
@[simp]
theorem NNReal.coe_eq_one (r : NNReal) :
r = 1 r = 1
theorem NNReal.coe_ne_zero {r : NNReal} :
r 0 r 0

Coercion ℝ≥0 → ℝ as a RingHom.

Porting note: todo: what if we define Coe ℝ≥0 ℝ using this function?

Instances For
@[simp]

A MulAction over ℝ restricts to a MulAction over ℝ≥0.

theorem NNReal.smul_def {M : Type u_1} [] (c : NNReal) (x : M) :
c x = c x
instance NNReal.smulCommClass_left {M : Type u_1} {N : Type u_2} [] [SMul M N] [] :
instance NNReal.smulCommClass_right {M : Type u_1} {N : Type u_2} [] [SMul M N] [] :

A DistribMulAction over ℝ restricts to a DistribMulAction over ℝ≥0.

A Module over ℝ restricts to a Module over ℝ≥0.

An Algebra over ℝ restricts to an Algebra over ℝ≥0.

@[simp]
theorem NNReal.coe_indicator {α : Type u_1} (s : Set α) (f : αNNReal) (a : α) :
↑() = Set.indicator s (fun x => ↑(f x)) a
@[simp]
theorem NNReal.coe_pow (r : NNReal) (n : ) :
↑(r ^ n) = r ^ n
@[simp]
theorem NNReal.coe_zpow (r : NNReal) (n : ) :
↑(r ^ n) = r ^ n
theorem NNReal.coe_list_sum (l : ) :
↑() =
theorem NNReal.coe_list_prod (l : ) :
↑() =
theorem NNReal.coe_sum {α : Type u_1} {s : } {f : αNNReal} :
↑(Finset.sum s fun a => f a) = Finset.sum s fun a => ↑(f a)
theorem Real.toNNReal_sum_of_nonneg {α : Type u_1} {s : } {f : α} (hf : ∀ (a : α), a s0 f a) :
Real.toNNReal (Finset.sum s fun a => f a) = Finset.sum s fun a => Real.toNNReal (f a)
theorem NNReal.coe_prod {α : Type u_1} {s : } {f : αNNReal} :
↑(Finset.prod s fun a => f a) = Finset.prod s fun a => ↑(f a)
theorem Real.toNNReal_prod_of_nonneg {α : Type u_1} {s : } {f : α} (hf : ∀ (a : α), a s0 f a) :
Real.toNNReal (Finset.prod s fun a => f a) = Finset.prod s fun a => Real.toNNReal (f a)
theorem NNReal.coe_nsmul (r : NNReal) (n : ) :
↑(n r) = n r
@[simp]
theorem NNReal.coe_nat_cast (n : ) :
n = n
@[simp]
theorem NNReal.coe_ofNat (n : ) [] :
↑() =
@[simp]
theorem NNReal.coe_le_coe {r₁ : NNReal} {r₂ : NNReal} :
r₁ r₂ r₁ r₂
@[simp]
theorem NNReal.coe_lt_coe {r₁ : NNReal} {r₂ : NNReal} :
r₁ < r₂ r₁ < r₂
@[simp]
theorem NNReal.coe_pos {r : NNReal} :
0 < r 0 < r
theorem NNReal.toReal_le_toReal {x : NNReal} {y : NNReal} (h : x y) :
x y
@[simp]
theorem Real.toNNReal_coe {r : NNReal} :
= r
@[simp]
theorem NNReal.mk_coe_nat (n : ) :
{ val := n, property := (_ : 0 n) } = n
@[simp]
theorem NNReal.toNNReal_coe_nat (n : ) :
= n
@[simp]
theorem Real.toNNReal_ofNat (n : ) [] :
noncomputable def NNReal.gi :

Real.toNNReal and NNReal.toReal : ℝ≥0 → ℝ form a Galois insertion.

Instances For
def NNReal.orderIsoIccZeroCoe (a : NNReal) :
↑(Set.Icc 0 a) ≃o ↑()

If a is a nonnegative real number, then the closed interval [0, a] in ℝ is order isomorphic to the interval Set.Iic a.

Instances For
@[simp]
theorem NNReal.orderIsoIccZeroCoe_apply_coe_coe (a : NNReal) (b : ↑(Set.Icc 0 a)) :
↑() = b
@[simp]
theorem NNReal.orderIsoIccZeroCoe_symm_apply_coe (a : NNReal) (b : ↑()) :
↑() = b
theorem NNReal.coe_image {s : } :
= {x | h, { val := x, property := h } s}
theorem NNReal.bddAbove_coe {s : } :
theorem NNReal.bddBelow_coe (s : ) :
theorem NNReal.coe_sSup (s : ) :
↑(sSup s) = sSup ()
@[simp]
theorem NNReal.coe_iSup {ι : Sort u_1} (s : ιNNReal) :
↑(⨆ (i : ι), s i) = ⨆ (i : ι), ↑(s i)
theorem NNReal.coe_sInf (s : ) :
↑(sInf s) = sInf ()
@[simp]
theorem NNReal.sInf_empty :
= 0
theorem NNReal.coe_iInf {ι : Sort u_1} (s : ιNNReal) :
↑(⨅ (i : ι), s i) = ⨅ (i : ι), ↑(s i)
theorem NNReal.le_iInf_add_iInf {ι : Sort u_1} {ι' : Sort u_2} [] [Nonempty ι'] {f : ιNNReal} {g : ι'NNReal} {a : NNReal} (h : ∀ (i : ι) (j : ι'), a f i + g j) :
a (⨅ (i : ι), f i) + ⨅ (j : ι'), g j
CovariantClass NNReal NNReal (fun x x_1 => x + x_1) fun x x_1 => x x_1
ContravariantClass NNReal NNReal (fun x x_1 => x + x_1) fun x x_1 => x < x_1
instance NNReal.covariant_mul :
CovariantClass NNReal NNReal (fun x x_1 => x * x_1) fun x x_1 => x x_1
theorem NNReal.le_of_forall_pos_le_add {a : NNReal} {b : NNReal} (h : ∀ (ε : NNReal), 0 < εa b + ε) :
a b
theorem NNReal.lt_iff_exists_rat_btwn (a : NNReal) (b : NNReal) :
a < b q, 0 q a < < b
theorem NNReal.mul_sup (a : NNReal) (b : NNReal) (c : NNReal) :
a * (b c) = a * b a * c
theorem NNReal.sup_mul (a : NNReal) (b : NNReal) (c : NNReal) :
(a b) * c = a * c b * c
theorem NNReal.mul_finset_sup {α : Type u_1} (r : NNReal) (s : ) (f : αNNReal) :
r * = Finset.sup s fun a => r * f a
theorem NNReal.finset_sup_mul {α : Type u_1} (s : ) (f : αNNReal) (r : NNReal) :
* r = Finset.sup s fun a => f a * r
theorem NNReal.finset_sup_div {α : Type u_1} {f : αNNReal} {s : } (r : NNReal) :
/ r = Finset.sup s fun a => f a / r
@[simp]
theorem NNReal.coe_max (x : NNReal) (y : NNReal) :
↑(max x y) = max x y
@[simp]
theorem NNReal.coe_min (x : NNReal) (y : NNReal) :
↑(min x y) = min x y
@[simp]
theorem NNReal.zero_le_coe {q : NNReal} :
0 q
@[simp]
theorem Real.coe_toNNReal' (r : ) :
↑() = max r 0
@[simp]
@[simp]
@[simp]
theorem Real.toNNReal_pos {r : } :
0 < r
@[simp]
theorem Real.toNNReal_eq_zero {r : } :
r 0
theorem Real.toNNReal_of_nonpos {r : } :
r 0
@[simp]
theorem Real.toNNReal_le_toNNReal_iff {r : } {p : } (hp : 0 p) :
r p
@[simp]
theorem Real.toNNReal_eq_toNNReal_iff {r : } {p : } (hr : 0 r) (hp : 0 p) :
r = p
@[simp]
theorem Real.toNNReal_lt_toNNReal_iff' {r : } {p : } :
r < p 0 < p
theorem Real.toNNReal_lt_toNNReal_iff {r : } {p : } (h : 0 < p) :
r < p
theorem Real.toNNReal_lt_toNNReal_iff_of_nonneg {r : } {p : } (hr : 0 r) :
r < p
@[simp]
theorem Real.toNNReal_add {r : } {p : } (hr : 0 r) (hp : 0 p) :
theorem Real.toNNReal_add_toNNReal {r : } {p : } (hr : 0 r) (hp : 0 p) :
theorem Real.toNNReal_le_toNNReal {r : } {p : } (h : r p) :
theorem Real.toNNReal_add_le {r : } {p : } :
theorem Real.toNNReal_le_iff_le_coe {r : } {p : NNReal} :
r p
theorem Real.le_toNNReal_iff_coe_le {r : NNReal} {p : } (hp : 0 p) :
r p
theorem Real.le_toNNReal_iff_coe_le' {r : NNReal} {p : } (hr : 0 < r) :
r p
theorem Real.toNNReal_lt_iff_lt_coe {r : } {p : NNReal} (ha : 0 r) :
r < p
theorem Real.lt_toNNReal_iff_coe_lt {r : NNReal} {p : } :
r < p
theorem Real.toNNReal_pow {x : } (hx : 0 x) (n : ) :
theorem Real.toNNReal_mul {p : } {q : } (hp : 0 p) :
theorem NNReal.mul_eq_mul_left {a : NNReal} {b : NNReal} {c : NNReal} (h : a 0) :
a * b = a * c b = c
theorem NNReal.pow_antitone_exp {a : NNReal} (m : ) (n : ) (mn : m n) (a1 : a 1) :
a ^ n a ^ m
theorem NNReal.exists_pow_lt_of_lt_one {a : NNReal} {b : NNReal} (ha : 0 < a) (hb : b < 1) :
n, b ^ n < a
theorem NNReal.exists_mem_Ico_zpow {x : NNReal} {y : NNReal} (hx : x 0) (hy : 1 < y) :
n, x Set.Ico (y ^ n) (y ^ (n + 1))
theorem NNReal.exists_mem_Ioc_zpow {x : NNReal} {y : NNReal} (hx : x 0) (hy : 1 < y) :
n, x Set.Ioc (y ^ n) (y ^ (n + 1))

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.

theorem NNReal.sub_def {r : NNReal} {p : NNReal} :
r - p = Real.toNNReal (r - p)
theorem NNReal.coe_sub_def {r : NNReal} {p : NNReal} :
↑(r - p) = max (r - p) 0
theorem NNReal.sub_div (a : NNReal) (b : NNReal) (c : NNReal) :
(a - b) / c = a / c - b / c
theorem NNReal.sum_div {ι : Type u_1} (s : ) (f : ιNNReal) (b : NNReal) :
(Finset.sum s fun i => f i) / b = Finset.sum s fun i => f i / b
@[simp]
theorem NNReal.inv_le {r : NNReal} {p : NNReal} (h : r 0) :
r⁻¹ p 1 r * p
theorem NNReal.inv_le_of_le_mul {r : NNReal} {p : NNReal} (h : 1 r * p) :
@[simp]
theorem NNReal.le_inv_iff_mul_le {r : NNReal} {p : NNReal} (h : p 0) :
r p⁻¹ r * p 1
@[simp]
theorem NNReal.lt_inv_iff_mul_lt {r : NNReal} {p : NNReal} (h : p 0) :
r < p⁻¹ r * p < 1
theorem NNReal.mul_le_iff_le_inv {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
r * a b a r⁻¹ * b
theorem NNReal.le_div_iff_mul_le {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
a b / r a * r b
theorem NNReal.div_le_iff {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
a / r b a b * r
theorem NNReal.div_le_iff' {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
a / r b a r * b
theorem NNReal.div_le_of_le_mul {a : NNReal} {b : NNReal} {c : NNReal} (h : a b * c) :
a / c b
theorem NNReal.div_le_of_le_mul' {a : NNReal} {b : NNReal} {c : NNReal} (h : a b * c) :
a / b c
theorem NNReal.le_div_iff {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
a b / r a * r b
theorem NNReal.le_div_iff' {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
a b / r r * a b
theorem NNReal.div_lt_iff {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
a / r < b a < b * r
theorem NNReal.div_lt_iff' {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
a / r < b a < r * b
theorem NNReal.lt_div_iff {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
a < b / r a * r < b
theorem NNReal.lt_div_iff' {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
a < b / r r * a < b
theorem NNReal.mul_lt_of_lt_div {a : NNReal} {b : NNReal} {r : NNReal} (h : a < b / r) :
a * r < b
theorem NNReal.div_le_div_left_of_le {a : NNReal} {b : NNReal} {c : NNReal} (c0 : c 0) (cb : c b) :
a / b a / c
theorem NNReal.div_le_div_left {a : NNReal} {b : NNReal} {c : NNReal} (a0 : 0 < a) (b0 : 0 < b) (c0 : 0 < c) :
a / b a / c c b
theorem NNReal.le_of_forall_lt_one_mul_le {x : NNReal} {y : NNReal} (h : ∀ (a : NNReal), a < 1a * x y) :
x y
theorem NNReal.half_le_self (a : NNReal) :
a / 2 a
theorem NNReal.half_lt_self {a : NNReal} (h : a 0) :
a / 2 < a
theorem NNReal.div_lt_one_of_lt {a : NNReal} {b : NNReal} (h : a < b) :
a / b < 1
theorem Real.toNNReal_div {x : } {y : } (hx : 0 x) :
theorem Real.toNNReal_div' {x : } {y : } (hy : 0 y) :
theorem NNReal.inv_lt_one_iff {x : NNReal} (hx : x 0) :
x⁻¹ < 1 1 < x
theorem NNReal.zpow_pos {x : NNReal} (hx : x 0) (n : ) :
0 < x ^ n
theorem NNReal.inv_lt_inv {x : NNReal} {y : NNReal} (hx : x 0) (h : x < y) :
@[simp]
theorem NNReal.abs_eq (x : NNReal) :
|x| = x
theorem NNReal.le_toNNReal_of_coe_le {x : NNReal} {y : } (h : x y) :
theorem NNReal.sSup_of_not_bddAbove {s : } (hs : ) :
sSup s = 0
theorem NNReal.iSup_of_not_bddAbove {ι : Sort u_1} {f : ιNNReal} (hf : ¬) :
⨆ (i : ι), f i = 0
theorem NNReal.iSup_empty {ι : Sort u_1} [] (f : ιNNReal) :
⨆ (i : ι), f i = 0
theorem NNReal.iInf_empty {ι : Sort u_1} [] (f : ιNNReal) :
⨅ (i : ι), f i = 0
@[simp]
theorem NNReal.iInf_const_zero {α : Sort u_2} :
⨅ (x : α), 0 = 0
theorem NNReal.iInf_mul {ι : Sort u_1} (f : ιNNReal) (a : NNReal) :
iInf f * a = ⨅ (i : ι), f i * a
theorem NNReal.mul_iInf {ι : Sort u_1} (f : ιNNReal) (a : NNReal) :
a * iInf f = ⨅ (i : ι), a * f i
theorem NNReal.mul_iSup {ι : Sort u_1} (f : ιNNReal) (a : NNReal) :
a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i
theorem NNReal.iSup_mul {ι : Sort u_1} (f : ιNNReal) (a : NNReal) :
(⨆ (i : ι), f i) * a = ⨆ (i : ι), f i * a
theorem NNReal.iSup_div {ι : Sort u_1} (f : ιNNReal) (a : NNReal) :
(⨆ (i : ι), f i) / a = ⨆ (i : ι), f i / a
theorem NNReal.mul_iSup_le {ι : Sort u_1} {a : NNReal} {g : NNReal} {h : ιNNReal} (H : ∀ (j : ι), g * h j a) :
g * iSup h a
theorem NNReal.iSup_mul_le {ι : Sort u_1} {a : NNReal} {g : ιNNReal} {h : NNReal} (H : ∀ (i : ι), g i * h a) :
iSup g * h a
theorem NNReal.iSup_mul_iSup_le {ι : Sort u_1} {a : NNReal} {g : ιNNReal} {h : ιNNReal} (H : ∀ (i j : ι), g i * h j a) :
iSup g * iSup h a
theorem NNReal.le_mul_iInf {ι : Sort u_1} [] {a : NNReal} {g : NNReal} {h : ιNNReal} (H : ∀ (j : ι), a g * h j) :
a g * iInf h
theorem NNReal.le_iInf_mul {ι : Sort u_1} [] {a : NNReal} {g : ιNNReal} {h : NNReal} (H : ∀ (i : ι), a g i * h) :
a iInf g * h
theorem NNReal.le_iInf_mul_iInf {ι : Sort u_1} [] {a : NNReal} {g : ιNNReal} {h : ιNNReal} (H : ∀ (i j : ι), a g i * h j) :
a iInf g * iInf h

The absolute value on ℝ as a map to ℝ≥0.

Instances For
@[simp]
theorem Real.coe_nnabs (x : ) :
↑() = |x|
@[simp]
theorem Real.nnabs_of_nonneg {x : } (h : 0 x) :
theorem Real.nnabs_coe (x : NNReal) :
Real.nnabs x = x
theorem Real.coe_toNNReal_le (x : ) :
↑() |x|

Extension for the positivity tactic: cast from ℝ≥0 to ℝ.

Instances For