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, conditionally_complete_linear_order_bot;

• 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:

• linear_ordered_semiring ℝ≥0;
• ordered_comm_semiring ℝ≥0;
• canonically_ordered_comm_semiring ℝ≥0;
• linear_ordered_comm_group_with_zero ℝ≥0;
• canonically_linear_ordered_add_monoid ℝ≥0;
• archimedean ℝ≥0;
• conditionally_complete_linear_order_bot ℝ≥0.

These instances are derived from corresponding instances about the type {x : α // 0 ≤ x} in an appropriate ordered field/ring/group/monoid α. See algebra/order/nonneg.

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

We also define an instance can_lift ℝ ℝ≥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 occurences 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.

## TODO #

semifield instance

@[protected, instance]
noncomputable def nnreal.linear_ordered_semiring  :
@[protected, instance]
@[protected, instance]
@[protected, instance]
noncomputable def nnreal.semilattice_inf  :
@[protected, instance]
noncomputable def nnreal.floor_semiring  :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
noncomputable def nnreal.has_sub  :
@[protected, instance]
noncomputable def nnreal.has_ordered_sub  :
@[protected, instance]
@[protected, instance]
def nnreal  :
Type

Nonnegative real numbers.

Equations
Instances for nnreal
@[protected, instance]
noncomputable def nnreal.has_div  :
@[protected, instance]
Equations
@[simp]
theorem nnreal.val_eq_coe (n : nnreal) :
n.val = n
@[protected, instance]
Equations
@[protected]
theorem nnreal.eq {n m : nnreal} :
n = mn = m
@[protected]
theorem nnreal.eq_iff {n m : nnreal} :
n = m n = m
theorem nnreal.ne_iff {x y : nnreal} :
x y x y
@[protected]
theorem nnreal.forall {p : nnreal → Prop} :
(∀ (x : nnreal), p x) ∀ (x : ) (hx : 0 x), p x, hx⟩
@[protected]
theorem nnreal.exists {p : nnreal → Prop} :
(∃ (x : nnreal), p x) ∃ (x : ) (hx : 0 x), p x, hx⟩
noncomputable def real.to_nnreal (r : ) :

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

Equations
theorem real.coe_to_nnreal (r : ) (hr : 0 r) :
theorem nnreal.coe_nonneg (r : nnreal) :
0 r
@[norm_cast]
theorem nnreal.coe_mk (a : ) (ha : 0 a) :
a, ha⟩ = a
@[protected]
@[protected, simp, norm_cast]
theorem nnreal.coe_eq {r₁ r₂ : nnreal} :
r₁ = r₂ r₁ = r₂
@[protected]
theorem nnreal.coe_zero  :
0 = 0
@[protected]
theorem nnreal.coe_one  :
1 = 1
@[protected]
theorem nnreal.coe_add (r₁ r₂ : nnreal) :
(r₁ + r₂) = r₁ + r₂
@[protected]
theorem nnreal.coe_mul (r₁ r₂ : nnreal) :
(r₁ * r₂) = r₁ * r₂
@[protected]
theorem nnreal.coe_inv (r : nnreal) :
@[protected]
theorem nnreal.coe_div (r₁ r₂ : nnreal) :
(r₁ / r₂) = r₁ / r₂
@[protected, simp, norm_cast]
theorem nnreal.coe_bit0 (r : nnreal) :
(bit0 r) =
@[protected, simp, norm_cast]
theorem nnreal.coe_bit1 (r : nnreal) :
(bit1 r) =
@[protected]
theorem nnreal.coe_two  :
2 = 2
@[protected, simp, norm_cast]
theorem nnreal.coe_sub {r₁ r₂ : nnreal} (h : r₂ r₁) :
(r₁ - r₂) = r₁ - r₂
@[protected, simp, norm_cast]
theorem nnreal.coe_eq_zero (r : nnreal) :
r = 0 r = 0
@[protected, simp, norm_cast]
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 ring_hom.

Equations
@[simp]
@[protected, instance]
def nnreal.mul_action {M : Type u_1} [ M] :

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

Equations
theorem nnreal.smul_def {M : Type u_1} [ M] (c : nnreal) (x : M) :
c x = c x
@[protected, instance]
def nnreal.is_scalar_tower {M : Type u_1} {N : Type u_2} [ M] [ N] [ N] [ N] :
@[protected, instance]
def nnreal.smul_comm_class_left {M : Type u_1} {N : Type u_2} [ N] [ N] [ N] :
@[protected, instance]
def nnreal.smul_comm_class_right {M : Type u_1} {N : Type u_2} [ N] [ N] [ N] :
@[protected, instance]
def nnreal.distrib_mul_action {M : Type u_1} [add_monoid M]  :

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

Equations
@[protected, instance]
def nnreal.module {M : Type u_1} [ M] :

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

Equations
@[protected, instance]
def nnreal.algebra {A : Type u_1} [semiring A] [ A] :

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

Equations
@[simp, norm_cast]
theorem nnreal.coe_indicator {α : Type u_1} (s : set α) (f : α → nnreal) (a : α) :
(s.indicator f a) = s.indicator (λ (x : α), (f x)) a
@[simp, norm_cast]
theorem nnreal.coe_pow (r : nnreal) (n : ) :
(r ^ n) = r ^ n
@[simp, norm_cast]
theorem nnreal.coe_zpow (r : nnreal) (n : ) :
(r ^ n) = r ^ n
@[norm_cast]
theorem nnreal.coe_list_sum (l : list nnreal) :
(l.sum) = l).sum
@[norm_cast]
theorem nnreal.coe_list_prod (l : list nnreal) :
(l.prod) = l).prod
@[norm_cast]
@[norm_cast]
@[norm_cast]
theorem nnreal.coe_sum {α : Type u_1} {s : finset α} {f : α → nnreal} :
(s.sum (λ (a : α), f a)) = s.sum (λ (a : α), (f a))
theorem real.to_nnreal_sum_of_nonneg {α : Type u_1} {s : finset α} {f : α → } (hf : ∀ (a : α), a s0 f a) :
(s.sum (λ (a : α), f a)).to_nnreal = s.sum (λ (a : α), (f a).to_nnreal)
@[norm_cast]
theorem nnreal.coe_prod {α : Type u_1} {s : finset α} {f : α → nnreal} :
(s.prod (λ (a : α), f a)) = s.prod (λ (a : α), (f a))
theorem real.to_nnreal_prod_of_nonneg {α : Type u_1} {s : finset α} {f : α → } (hf : ∀ (a : α), a s0 f a) :
(s.prod (λ (a : α), f a)).to_nnreal = s.prod (λ (a : α), (f a).to_nnreal)
theorem nnreal.nsmul_coe (r : nnreal) (n : ) :
(n r) = n r
@[protected, simp, norm_cast]
theorem nnreal.coe_nat_cast (n : ) :
@[protected, simp, norm_cast]
theorem nnreal.coe_le_coe {r₁ r₂ : nnreal} :
r₁ r₂ r₁ r₂
@[protected, simp, norm_cast]
theorem nnreal.coe_lt_coe {r₁ r₂ : nnreal} :
r₁ < r₂ r₁ < r₂
@[protected, simp, norm_cast]
theorem nnreal.coe_pos {r : nnreal} :
0 < r 0 < r
@[protected]
theorem nnreal.coe_mono  :
@[protected]
@[simp]
theorem real.to_nnreal_coe {r : nnreal} :
@[simp]
theorem nnreal.mk_coe_nat (n : ) :
n, _⟩ = n
@[simp]
noncomputable def nnreal.gi  :

real.to_nnreal and coe : ℝ≥0 → ℝ form a Galois insertion.

Equations
@[simp]
theorem nnreal.order_iso_Icc_zero_coe_apply_coe_coe (a : nnreal) (ᾰ : {x // x (λ (x : ), x a) x}) :

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

Equations
theorem nnreal.coe_image {s : set nnreal} :
= {x : | ∃ (h : 0 x), x, h⟩ s}
@[protected, instance]
Equations
@[norm_cast]
@[norm_cast]
theorem nnreal.coe_supr {ι : Sort u_1} (s : ι → nnreal) :
(⨆ (i : ι), s i) = ⨆ (i : ι), (s i)
@[norm_cast]
@[simp]
theorem nnreal.Inf_empty  :
@[norm_cast]
theorem nnreal.coe_infi {ι : Sort u_1} (s : ι → nnreal) :
(⨅ (i : ι), s i) = ⨅ (i : ι), (s i)
theorem nnreal.le_infi_add_infi {ι : Sort u_1} {ι' : Sort u_2} [nonempty ι] [nonempty ι'] {f : ι → nnreal} {g : ι' → nnreal} {a : nnreal} (h : ∀ (i : ι) (j : ι'), a f i + g j) :
a (⨅ (i : ι), f i) + ⨅ (j : ι'), g j
@[protected, instance]
@[protected, instance]
@[protected, instance]
theorem nnreal.le_of_forall_pos_le_add {a b : nnreal} (h : ∀ (ε : nnreal), 0 < εa b + ε) :
a b
theorem nnreal.lt_iff_exists_rat_btwn (a b : nnreal) :
a < b ∃ (q : ), 0 q a < q.to_nnreal q.to_nnreal < b
theorem nnreal.bot_eq_zero  :
= 0
theorem nnreal.mul_sup (a b c : nnreal) :
a * (b c) = a * b a * c
theorem nnreal.sup_mul (a b c : nnreal) :
(a b) * c = a * c b * c
theorem nnreal.mul_finset_sup {α : Type u_1} (r : nnreal) (s : finset α) (f : α → nnreal) :
r * s.sup f = s.sup (λ (a : α), r * f a)
theorem nnreal.finset_sup_mul {α : Type u_1} (s : finset α) (f : α → nnreal) (r : nnreal) :
s.sup f * r = s.sup (λ (a : α), f a * r)
theorem nnreal.finset_sup_div {α : Type u_1} {f : α → nnreal} {s : finset α} (r : nnreal) :
s.sup f / r = s.sup (λ (a : α), f a / r)
@[simp, norm_cast]
theorem nnreal.coe_max (x y : nnreal) :
y) =
@[simp, norm_cast]
theorem nnreal.coe_min (x y : nnreal) :
y) =
@[simp]
theorem nnreal.zero_le_coe {q : nnreal} :
0 q
@[simp]
theorem real.to_nnreal_zero  :
@[simp]
theorem real.to_nnreal_one  :
@[simp]
theorem real.to_nnreal_pos {r : } :
0 < r.to_nnreal 0 < r
@[simp]
theorem real.to_nnreal_eq_zero {r : } :
r.to_nnreal = 0 r 0
theorem real.to_nnreal_of_nonpos {r : } :
r 0r.to_nnreal = 0
@[simp]
theorem real.coe_to_nnreal' (r : ) :
@[simp]
theorem real.to_nnreal_le_to_nnreal_iff {r p : } (hp : 0 p) :
r p
@[simp]
theorem real.to_nnreal_lt_to_nnreal_iff' {r p : } :
r < p 0 < p
theorem real.to_nnreal_lt_to_nnreal_iff {r p : } (h : 0 < p) :
r < p
theorem real.to_nnreal_lt_to_nnreal_iff_of_nonneg {r p : } (hr : 0 r) :
r < p
@[simp]
theorem real.to_nnreal_add {r p : } (hr : 0 r) (hp : 0 p) :
(r + p).to_nnreal =
theorem real.to_nnreal_add_to_nnreal {r p : } (hr : 0 r) (hp : 0 p) :
= (r + p).to_nnreal
theorem real.to_nnreal_le_to_nnreal {r p : } (h : r p) :
theorem real.to_nnreal_add_le {r p : } :
(r + p).to_nnreal
theorem real.le_to_nnreal_iff_coe_le {r : nnreal} {p : } (hp : 0 p) :
theorem real.le_to_nnreal_iff_coe_le' {r : nnreal} {p : } (hr : 0 < r) :
theorem real.to_nnreal_lt_iff_lt_coe {r : } {p : nnreal} (ha : 0 r) :
theorem real.lt_to_nnreal_iff_coe_lt {r : nnreal} {p : } :
@[simp]
theorem real.to_nnreal_bit0 (r : ) :
@[simp]
theorem real.to_nnreal_bit1 {r : } (hr : 0 r) :
theorem nnreal.mul_eq_mul_left {a b c : nnreal} (h : a 0) :
a * b = a * c b = c
theorem real.to_nnreal_mul {p q : } (hp : 0 p) :
(p * q).to_nnreal =
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 b : nnreal} (ha : 0 < a) (hb : b < 1) :
∃ (n : ), b ^ n < a
theorem nnreal.exists_mem_Ico_zpow {x y : nnreal} (hx : x 0) (hy : 1 < y) :
∃ (n : ), x set.Ico (y ^ n) (y ^ (n + 1))
theorem nnreal.exists_mem_Ioc_zpow {x 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 has_ordered_sub in the file algebra.order.sub. See also mul_tsub and tsub_mul.

theorem nnreal.sub_def {r p : nnreal} :
r - p = (r - p).to_nnreal
theorem nnreal.coe_sub_def {r p : nnreal} :
theorem nnreal.sub_div (a b c : nnreal) :
(a - b) / c = a / c - b / c
theorem nnreal.sum_div {ι : Type u_1} (s : finset ι) (f : ι → nnreal) (b : nnreal) :
s.sum (λ (i : ι), f i) / b = s.sum (λ (i : ι), f i / b)
@[simp]
theorem nnreal.inv_pos {r : nnreal} :
0 < r⁻¹ 0 < r
theorem nnreal.div_pos {r p : nnreal} (hr : 0 < r) (hp : 0 < p) :
0 < r / p
theorem nnreal.div_self_le (r : nnreal) :
r / r 1
@[simp]
theorem nnreal.inv_le {r p : nnreal} (h : r 0) :
r⁻¹ p 1 r * p
theorem nnreal.inv_le_of_le_mul {r p : nnreal} (h : 1 r * p) :
@[simp]
theorem nnreal.le_inv_iff_mul_le {r p : nnreal} (h : p 0) :
r p⁻¹ r * p 1
@[simp]
theorem nnreal.lt_inv_iff_mul_lt {r p : nnreal} (h : p 0) :
r < p⁻¹ r * p < 1
theorem nnreal.mul_le_iff_le_inv {a b r : nnreal} (hr : r 0) :
r * a b a r⁻¹ * b
theorem nnreal.le_div_iff_mul_le {a b r : nnreal} (hr : r 0) :
a b / r a * r b
theorem nnreal.div_le_iff {a b r : nnreal} (hr : r 0) :
a / r b a b * r
theorem nnreal.div_le_iff' {a b r : nnreal} (hr : r 0) :
a / r b a r * b
theorem nnreal.div_le_of_le_mul {a b c : nnreal} (h : a b * c) :
a / c b
theorem nnreal.div_le_of_le_mul' {a b c : nnreal} (h : a b * c) :
a / b c
theorem nnreal.le_div_iff {a b r : nnreal} (hr : r 0) :
a b / r a * r b
theorem nnreal.le_div_iff' {a b r : nnreal} (hr : r 0) :
a b / r r * a b
theorem nnreal.div_lt_iff {a b r : nnreal} (hr : r 0) :
a / r < b a < b * r
theorem nnreal.div_lt_iff' {a b r : nnreal} (hr : r 0) :
a / r < b a < r * b
theorem nnreal.lt_div_iff {a b r : nnreal} (hr : r 0) :
a < b / r a * r < b
theorem nnreal.lt_div_iff' {a b r : nnreal} (hr : r 0) :
a < b / r r * a < b
theorem nnreal.mul_lt_of_lt_div {a b r : nnreal} (h : a < b / r) :
a * r < b
theorem nnreal.div_le_div_left_of_le {a b c : nnreal} (b0 : 0 < b) (c0 : 0 < c) (cb : c b) :
a / b a / c
theorem nnreal.div_le_div_left {a b 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 y : nnreal} (h : ∀ (a : nnreal), a < 1a * x y) :
x y
theorem nnreal.div_add_div_same (a b c : nnreal) :
a / c + b / c = (a + b) / c
theorem nnreal.half_pos {a : nnreal} (h : 0 < a) :
0 < a / 2
theorem nnreal.add_halves (a : nnreal) :
a / 2 + a / 2 = a
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 b : nnreal} (h : a < b) :
a / b < 1
theorem nnreal.div_add_div (a : nnreal) {b : nnreal} (c : nnreal) {d : nnreal} (hb : b 0) (hd : d 0) :
a / b + c / d = (a * d + b * c) / (b * d)
theorem nnreal.add_div' (a b c : nnreal) (hc : c 0) :
b + a / c = (b * c + a) / c
theorem nnreal.div_add' (a b c : nnreal) (hc : c 0) :
a / c + b = (a + b * c) / c
theorem real.to_nnreal_div {x y : } (hx : 0 x) :
(x / y).to_nnreal =
theorem real.to_nnreal_div' {x y : } (hy : 0 y) :
(x / y).to_nnreal =
theorem nnreal.inv_lt_one_iff {x : nnreal} (hx : x 0) :
x⁻¹ < 1 1 < x
theorem nnreal.inv_lt_one {x : nnreal} (hx : 1 < x) :
x⁻¹ < 1
theorem nnreal.zpow_pos {x : nnreal} (hx : x 0) (n : ) :
0 < x ^ n
theorem nnreal.inv_lt_inv_iff {x y : nnreal} (hx : x 0) (hy : y 0) :
y⁻¹ < x⁻¹ x < y
theorem nnreal.inv_lt_inv {x y : nnreal} (hx : x 0) (h : x < y) :
@[simp]
theorem nnreal.abs_eq (x : nnreal) :
theorem nnreal.le_to_nnreal_of_coe_le {x : nnreal} {y : } (h : x y) :
theorem nnreal.Sup_of_not_bdd_above {s : set nnreal} (hs : ¬) :
= 0
theorem nnreal.supr_of_not_bdd_above {ι : Sort u_1} {f : ι → nnreal} (hf : ¬) :
(⨆ (i : ι), f i) = 0
theorem nnreal.infi_empty {ι : Sort u_1} [is_empty ι] (f : ι → nnreal) :
(⨅ (i : ι), f i) = 0
@[simp]
theorem nnreal.infi_const_zero {α : Sort u_1} :
(⨅ (i : α), 0) = 0
theorem nnreal.infi_mul {ι : Sort u_1} (f : ι → nnreal) (a : nnreal) :
infi f * a = ⨅ (i : ι), f i * a
theorem nnreal.mul_infi {ι : Sort u_1} (f : ι → nnreal) (a : nnreal) :
a * infi f = ⨅ (i : ι), a * f i
theorem nnreal.mul_supr {ι : Sort u_1} (f : ι → nnreal) (a : nnreal) :
(a * ⨆ (i : ι), f i) = ⨆ (i : ι), a * f i
theorem nnreal.supr_mul {ι : Sort u_1} (f : ι → nnreal) (a : nnreal) :
(⨆ (i : ι), f i) * a = ⨆ (i : ι), f i * a
theorem nnreal.supr_div {ι : Sort u_1} (f : ι → nnreal) (a : nnreal) :
(⨆ (i : ι), f i) / a = ⨆ (i : ι), f i / a
theorem nnreal.le_mul_infi {ι : Sort u_1} [nonempty ι] {a g : nnreal} {h : ι → nnreal} (H : ∀ (j : ι), a g * h j) :
a g * infi h
theorem nnreal.mul_supr_le {ι : Sort u_1} [nonempty ι] {a g : nnreal} {h : ι → nnreal} (H : ∀ (j : ι), g * h j a) :
g * supr h a
theorem nnreal.le_infi_mul {ι : Sort u_1} [nonempty ι] {a : nnreal} {g : ι → nnreal} {h : nnreal} (H : ∀ (i : ι), a g i * h) :
a infi g * h
theorem nnreal.supr_mul_le {ι : Sort u_1} [nonempty ι] {a : nnreal} {g : ι → nnreal} {h : nnreal} (H : ∀ (i : ι), g i * h a) :
supr g * h a
theorem nnreal.le_infi_mul_infi {ι : Sort u_1} [nonempty ι] {a : nnreal} {g h : ι → nnreal} (H : ∀ (i j : ι), a g i * h j) :
a infi g * infi h
theorem nnreal.supr_mul_supr_le {ι : Sort u_1} [nonempty ι] {a : nnreal} {g h : ι → nnreal} (H : ∀ (i j : ι), g i * h j a) :
supr g * supr h a
noncomputable def real.nnabs  :

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

Equations
@[simp, norm_cast]
theorem real.coe_nnabs (x : ) :
@[simp]
theorem real.nnabs_of_nonneg {x : } (h : 0 x) :