mathlib documentation

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.

@[protected, instance]

noncomputable def nnreal.linear_ordered_semiring :

linear_ordered_semiring ℝ≥0

@[protected, instance]

def nnreal.canonically_ordered_comm_semiring :

canonically_ordered_comm_semiring ℝ≥0

@[protected, instance]

def nnreal.order_bot :

order_bot ℝ≥0

@[protected, instance]

noncomputable def nnreal.semilattice_inf :

semilattice_inf ℝ≥0

@[protected, instance]

noncomputable def nnreal.floor_semiring :

floor_semiring ℝ≥0

@[protected, instance]

def nnreal.inhabited :

inhabited ℝ≥0

@[protected, instance]

def nnreal.comm_monoid_with_zero :

comm_monoid_with_zero ℝ≥0

@[protected, instance]

def nnreal.archimedean :

archimedean ℝ≥0

@[protected, instance]

def nnreal.ordered_comm_semiring :

ordered_comm_semiring ℝ≥0

@[protected, instance]

def nnreal.ordered_semiring :

ordered_semiring ℝ≥0

@[protected, instance]

noncomputable def nnreal.linear_ordered_comm_group_with_zero :

linear_ordered_comm_group_with_zero ℝ≥0

@[protected, instance]

noncomputable def nnreal.has_sub :

has_sub ℝ≥0

@[protected, instance]

noncomputable def nnreal.has_ordered_sub :

has_ordered_sub ℝ≥0

@[protected, instance]

def nnreal.densely_ordered :

densely_ordered ℝ≥0

@[protected, instance]

noncomputable def nnreal.canonically_linear_ordered_add_monoid :

canonically_linear_ordered_add_monoid ℝ≥0

def nnreal :

Type

Nonnegative real numbers.

Equations

ℝ≥0 = {r // 0 ≤ r}

@[protected, instance]

noncomputable def nnreal.has_div :

has_div ℝ≥0

@[protected, instance]

def nnreal.real.has_coe :

has_coe ℝ≥0 ℝ

Equations

nnreal.real.has_coe = {coe := subtype.val (λ (r : ℝ), 0 ≤ r)}

@[simp]

theorem nnreal.val_eq_coe (n : ℝ≥0) :

@[protected, instance]

def nnreal.can_lift :

can_lift ℝ ℝ≥0

Equations

nnreal.can_lift = {coe := coe coe_to_lift, cond := λ (r : ℝ), 0 ≤ r, prf := nnreal.can_lift._proof_1}

@[protected]

theorem nnreal.eq {n m : ℝ≥0} :

↑n = ↑m → n = m

@[protected]

theorem nnreal.eq_iff {n m : ℝ≥0} :

↑n = ↑m ↔ n = m

theorem nnreal.ne_iff {x y : ℝ≥0} :

↑x ≠ ↑y ↔ x ≠ y

noncomputable def real.to_nnreal (r : ℝ) :

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

Equations

r.to_nnreal = ⟨max r 0, _⟩

theorem real.coe_to_nnreal (r : ℝ) (hr : 0 ≤ r) :

↑(r.to_nnreal) = r

theorem real.le_coe_to_nnreal (r : ℝ) :

r ≤ ↑(r.to_nnreal)

theorem nnreal.coe_nonneg (r : ℝ≥0) :

@[norm_cast]

theorem nnreal.coe_mk (a : ℝ) (ha : 0 ≤ a) :

↑⟨a, ha⟩ = a

@[protected]

theorem nnreal.coe_injective :

function.injective coe

@[protected, simp, norm_cast]

theorem nnreal.coe_eq {r₁ r₂ : ℝ≥0} :

↑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₂ : ℝ≥0) :

↑(r₁ + r₂) = ↑r₁ + ↑r₂

@[protected]

theorem nnreal.coe_mul (r₁ r₂ : ℝ≥0) :

↑r₁ * r₂ = (↑r₁) * ↑r₂

@[protected]

theorem nnreal.coe_inv (r : ℝ≥0) :

↑r⁻¹ = (↑r)⁻¹

@[protected]

theorem nnreal.coe_div (r₁ r₂ : ℝ≥0) :

↑(r₁ / r₂) = ↑r₁ / ↑r₂

@[protected, simp, norm_cast]

theorem nnreal.coe_bit0 (r : ℝ≥0) :

↑(bit0 r) = bit0 ↑r

@[protected, simp, norm_cast]

theorem nnreal.coe_bit1 (r : ℝ≥0) :

↑(bit1 r) = bit1 ↑r

@[protected, simp, norm_cast]

theorem nnreal.coe_sub {r₁ r₂ : ℝ≥0} (h : r₂ ≤ r₁) :

↑(r₁ - r₂) = ↑r₁ - ↑r₂

@[protected, simp, norm_cast]

theorem nnreal.coe_eq_zero (r : ℝ≥0) :

↑r = 0 ↔ r = 0

@[protected, simp, norm_cast]

theorem nnreal.coe_eq_one (r : ℝ≥0) :

↑r = 1 ↔ r = 1

theorem nnreal.coe_ne_zero {r : ℝ≥0} :

↑r ≠ 0 ↔ r ≠ 0

def nnreal.to_real_hom :

ℝ≥0 →+* ℝ

Coercion ℝ≥0 → ℝ as a ring_hom.

Equations

nnreal.to_real_hom = {to_fun := coe coe_to_lift, map_one' := nnreal.coe_one, map_mul' := nnreal.coe_mul, map_zero' := nnreal.coe_zero, map_add' := nnreal.coe_add}

@[simp]

theorem nnreal.coe_to_real_hom :

⇑nnreal.to_real_hom = coe

@[protected, instance]

def nnreal.mul_action {M : Type u_1} [mul_action ℝ M] :

mul_action ℝ≥0 M

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

Equations

nnreal.mul_action = mul_action.comp_hom M nnreal.to_real_hom.to_monoid_hom

theorem nnreal.smul_def {M : Type u_1} [mul_action ℝ M] (c : ℝ≥0) (x : M) :

c • x = ↑c • x

@[protected, instance]

def nnreal.is_scalar_tower {M : Type u_1} {N : Type u_2} [mul_action ℝ M] [mul_action ℝ N] [has_scalar M N] [is_scalar_tower ℝ M N] :

is_scalar_tower ℝ≥0 M N

@[protected, instance]

def nnreal.smul_comm_class_left {M : Type u_1} {N : Type u_2} [mul_action ℝ N] [has_scalar M N] [smul_comm_class ℝ M N] :

smul_comm_class ℝ≥0 M N

@[protected, instance]

def nnreal.smul_comm_class_right {M : Type u_1} {N : Type u_2} [mul_action ℝ N] [has_scalar M N] [smul_comm_class M ℝ N] :

smul_comm_class M ℝ≥0 N

@[protected, instance]

def nnreal.distrib_mul_action {M : Type u_1} [add_monoid M] [distrib_mul_action ℝ M] :

distrib_mul_action ℝ≥0 M

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

Equations

nnreal.distrib_mul_action = distrib_mul_action.comp_hom M nnreal.to_real_hom.to_monoid_hom

@[protected, instance]

def nnreal.module {M : Type u_1} [add_comm_monoid M] [module ℝ M] :

module ℝ≥0 M

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

Equations

nnreal.module = module.comp_hom M nnreal.to_real_hom

@[protected, instance]

def nnreal.algebra {A : Type u_1} [semiring A] [algebra ℝ A] :

algebra ℝ≥0 A

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

Equations

nnreal.algebra = {to_has_scalar := {smul := has_scalar.smul smul_with_zero.to_has_scalar}, to_ring_hom := (algebra_map ℝ A).comp nnreal.to_real_hom, commutes' := _, smul_def' := _}

@[simp, norm_cast]

theorem nnreal.coe_indicator {α : Type u_1} (s : set α) (f : α → ℝ≥0) (a : α) :

↑(s.indicator f a) = s.indicator (λ (x : α), ↑(f x)) a

@[simp, norm_cast]

theorem nnreal.coe_pow (r : ℝ≥0) (n : ℕ) :

↑(r ^ n) = ↑r ^ n

@[simp, norm_cast]

theorem nnreal.coe_zpow (r : ℝ≥0) (n : ℤ) :

↑(r ^ n) = ↑r ^ n

@[norm_cast]

theorem nnreal.coe_list_sum (l : list ℝ≥0) :

↑(l.sum) = (list.map coe l).sum

@[norm_cast]

theorem nnreal.coe_list_prod (l : list ℝ≥0) :

↑(l.prod) = (list.map coe l).prod

@[norm_cast]

theorem nnreal.coe_multiset_sum (s : multiset ℝ≥0) :

↑(s.sum) = (multiset.map coe s).sum

@[norm_cast]

theorem nnreal.coe_multiset_prod (s : multiset ℝ≥0) :

↑(s.prod) = (multiset.map coe s).prod

@[norm_cast]

theorem nnreal.coe_sum {α : Type u_1} {s : finset α} {f : α → ℝ≥0} :

↑∑ (a : α) in s, f a = ∑ (a : α) in s, ↑(f a)

theorem real.to_nnreal_sum_of_nonneg {α : Type u_1} {s : finset α} {f : α → ℝ} (hf : ∀ (a : α), a ∈ s → 0 ≤ f a) :

(∑ (a : α) in s, f a).to_nnreal = ∑ (a : α) in s, (f a).to_nnreal

@[norm_cast]

theorem nnreal.coe_prod {α : Type u_1} {s : finset α} {f : α → ℝ≥0} :

↑∏ (a : α) in s, f a = ∏ (a : α) in s, ↑(f a)

theorem real.to_nnreal_prod_of_nonneg {α : Type u_1} {s : finset α} {f : α → ℝ} (hf : ∀ (a : α), a ∈ s → 0 ≤ f a) :

(∏ (a : α) in s, f a).to_nnreal = ∏ (a : α) in s, (f a).to_nnreal

theorem nnreal.nsmul_coe (r : ℝ≥0) (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₂ : ℝ≥0} :

↑r₁ ≤ ↑r₂ ↔ r₁ ≤ r₂

@[protected, simp, norm_cast]

theorem nnreal.coe_lt_coe {r₁ r₂ : ℝ≥0} :

↑r₁ < ↑r₂ ↔ r₁ < r₂

@[protected, simp, norm_cast]

theorem nnreal.coe_pos {r : ℝ≥0} :

0 < ↑r ↔ 0 < r

@[protected]

theorem nnreal.coe_mono :

@[protected]

theorem real.to_nnreal_mono :

monotone real.to_nnreal

@[simp]

theorem real.to_nnreal_coe {r : ℝ≥0} :

↑r.to_nnreal = r

@[simp]

theorem nnreal.mk_coe_nat (n : ℕ) :

⟨↑n, _⟩ = ↑n

@[simp]

theorem nnreal.to_nnreal_coe_nat (n : ℕ) :

↑n.to_nnreal = ↑n

noncomputable def nnreal.gi :

galois_insertion real.to_nnreal coe

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

Equations

nnreal.gi = galois_insertion.monotone_intro nnreal.coe_mono real.to_nnreal_mono real.le_coe_to_nnreal nnreal.gi._proof_1

theorem nnreal.coe_image {s : set ℝ≥0} :

coe '' s = {x : ℝ | ∃ (h : 0 ≤ x), ⟨x, h⟩ ∈ s}

theorem nnreal.bdd_above_coe {s : set ℝ≥0} :

bdd_above (coe '' s) ↔ bdd_above s

theorem nnreal.bdd_below_coe (s : set ℝ≥0) :

bdd_below (coe '' s)

@[protected, instance]

noncomputable def nnreal.conditionally_complete_linear_order_bot :

conditionally_complete_linear_order_bot ℝ≥0

Equations

nnreal.conditionally_complete_linear_order_bot = nonneg.conditionally_complete_linear_order_bot nnreal.conditionally_complete_linear_order_bot._proof_1

@[norm_cast]

theorem nnreal.coe_Sup (s : set ℝ≥0) :

↑(Sup s) = Sup (coe '' s)

@[norm_cast]

theorem nnreal.coe_supr {ι : Sort u_1} (s : ι → ℝ≥0) :

(↑⨆ (i : ι), s i) = ⨆ (i : ι), ↑(s i)

@[norm_cast]

theorem nnreal.coe_Inf (s : set ℝ≥0) :

↑(Inf s) = Inf (coe '' s)

@[norm_cast]

theorem nnreal.coe_infi {ι : Sort u_1} (s : ι → ℝ≥0) :

(↑⨅ (i : ι), s i) = ⨅ (i : ι), ↑(s i)

@[protected, instance]

def nnreal.covariant_add :

covariant_class ℝ≥0 ℝ≥0 has_add.add has_le.le

@[protected, instance]

def nnreal.contravariant_add :

contravariant_class ℝ≥0 ℝ≥0 has_add.add has_lt.lt

@[protected, instance]

def nnreal.covariant_mul :

covariant_class ℝ≥0 ℝ≥0 has_mul.mul has_le.le

theorem nnreal.le_of_forall_pos_le_add {a b : ℝ≥0} (h : ∀ (ε : ℝ≥0), 0 < ε → a ≤ b + ε) :

a ≤ b

theorem nnreal.le_of_add_le_left {a b c : ℝ≥0} (h : a + b ≤ c) :

a ≤ c

theorem nnreal.le_of_add_le_right {a b c : ℝ≥0} (h : a + b ≤ c) :

b ≤ c

theorem nnreal.lt_iff_exists_rat_btwn (a b : ℝ≥0) :

a < b ↔ ∃ (q : ℚ), 0 ≤ q ∧ a < ↑q.to_nnreal ∧ ↑q.to_nnreal < b

theorem nnreal.bot_eq_zero :

theorem nnreal.mul_sup (a b c : ℝ≥0) :

a * (b ⊔ c) = a * b ⊔ a * c

theorem nnreal.sup_mul (a b c : ℝ≥0) :

(a ⊔ b) * c = a * c ⊔ b * c

theorem nnreal.mul_finset_sup {α : Type u_1} (r : ℝ≥0) (s : finset α) (f : α → ℝ≥0) :

r * s.sup f = s.sup (λ (a : α), r * f a)

theorem nnreal.finset_sup_mul {α : Type u_1} (s : finset α) (f : α → ℝ≥0) (r : ℝ≥0) :

(s.sup f) * r = s.sup (λ (a : α), (f a) * r)

theorem nnreal.finset_sup_div {α : Type u_1} {f : α → ℝ≥0} {s : finset α} (r : ℝ≥0) :

s.sup f / r = s.sup (λ (a : α), f a / r)

@[simp, norm_cast]

theorem nnreal.coe_max (x y : ℝ≥0) :

↑(max x y) = max ↑x ↑y

@[simp, norm_cast]

theorem nnreal.coe_min (x y : ℝ≥0) :

↑(min x y) = min ↑x ↑y

@[simp]

theorem nnreal.zero_le_coe {q : ℝ≥0} :

@[simp]

theorem real.to_nnreal_zero :

0.to_nnreal = 0

@[simp]

theorem real.to_nnreal_one :

1.to_nnreal = 1

@[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 ≤ 0 → r.to_nnreal = 0

@[simp]

theorem real.coe_to_nnreal' (r : ℝ) :

↑(r.to_nnreal) = max r 0

@[simp]

theorem real.to_nnreal_le_to_nnreal_iff {r p : ℝ} (hp : 0 ≤ p) :

r.to_nnreal ≤ p.to_nnreal ↔ r ≤ p

@[simp]

theorem real.to_nnreal_lt_to_nnreal_iff' {r p : ℝ} :

r.to_nnreal < p.to_nnreal ↔ r < p ∧ 0 < p

theorem real.to_nnreal_lt_to_nnreal_iff {r p : ℝ} (h : 0 < p) :

r.to_nnreal < p.to_nnreal ↔ r < p

theorem real.to_nnreal_lt_to_nnreal_iff_of_nonneg {r p : ℝ} (hr : 0 ≤ r) :

r.to_nnreal < p.to_nnreal ↔ r < p

@[simp]

theorem real.to_nnreal_add {r p : ℝ} (hr : 0 ≤ r) (hp : 0 ≤ p) :

(r + p).to_nnreal = r.to_nnreal + p.to_nnreal

theorem real.to_nnreal_add_to_nnreal {r p : ℝ} (hr : 0 ≤ r) (hp : 0 ≤ p) :

r.to_nnreal + p.to_nnreal = (r + p).to_nnreal

theorem real.to_nnreal_le_to_nnreal {r p : ℝ} (h : r ≤ p) :

r.to_nnreal ≤ p.to_nnreal

theorem real.to_nnreal_add_le {r p : ℝ} :

(r + p).to_nnreal ≤ r.to_nnreal + p.to_nnreal

theorem real.to_nnreal_le_iff_le_coe {r : ℝ} {p : ℝ≥0} :

r.to_nnreal ≤ p ↔ r ≤ ↑p

theorem real.le_to_nnreal_iff_coe_le {r : ℝ≥0} {p : ℝ} (hp : 0 ≤ p) :

r ≤ p.to_nnreal ↔ ↑r ≤ p

theorem real.le_to_nnreal_iff_coe_le' {r : ℝ≥0} {p : ℝ} (hr : 0 < r) :

r ≤ p.to_nnreal ↔ ↑r ≤ p

theorem real.to_nnreal_lt_iff_lt_coe {r : ℝ} {p : ℝ≥0} (ha : 0 ≤ r) :

r.to_nnreal < p ↔ r < ↑p

theorem real.lt_to_nnreal_iff_coe_lt {r : ℝ≥0} {p : ℝ} :

r < p.to_nnreal ↔ ↑r < p

@[simp]

theorem real.to_nnreal_bit0 {r : ℝ} (hr : 0 ≤ r) :

(bit0 r).to_nnreal = bit0 r.to_nnreal

@[simp]

theorem real.to_nnreal_bit1 {r : ℝ} (hr : 0 ≤ r) :

(bit1 r).to_nnreal = bit1 r.to_nnreal

theorem nnreal.mul_eq_mul_left {a b c : ℝ≥0} (h : a ≠ 0) :

a * b = a * c ↔ b = c

theorem real.to_nnreal_mul {p q : ℝ} (hp : 0 ≤ p) :

(p * q).to_nnreal = (p.to_nnreal) * q.to_nnreal

theorem nnreal.pow_antitone_exp {a : ℝ≥0} (m n : ℕ) (mn : m ≤ n) (a1 : a ≤ 1) :

a ^ n ≤ a ^ m

theorem nnreal.exists_pow_lt_of_lt_one {a b : ℝ≥0} (ha : 0 < a) (hb : b < 1) :

∃ (n : ℕ), b ^ n < a

theorem nnreal.exists_mem_Ico_zpow {x y : ℝ≥0} (hx : x ≠ 0) (hy : 1 < y) :

∃ (n : ℤ), x ∈ set.Ico (y ^ n) (y ^ (n + 1))

theorem nnreal.exists_mem_Ioc_zpow {x y : ℝ≥0} (hx : x ≠ 0) (hy : 1 < y) :

∃ (n : ℤ), x ∈ set.Ioc (y ^ n) (y ^ (n + 1))

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 has_ordered_sub in the file algebra.order.sub. See also mul_tsub and tsub_mul.

theorem nnreal.sub_def {r p : ℝ≥0} :

r - p = (↑r - ↑p).to_nnreal

theorem nnreal.coe_sub_def {r p : ℝ≥0} :

↑(r - p) = max (↑r - ↑p) 0

theorem nnreal.sub_div (a b c : ℝ≥0) :

(a - b) / c = a / c - b / c

theorem nnreal.sum_div {ι : Type u_1} (s : finset ι) (f : ι → ℝ≥0) (b : ℝ≥0) :

(∑ (i : ι) in s, f i) / b = ∑ (i : ι) in s, f i / b

@[simp]

theorem nnreal.inv_pos {r : ℝ≥0} :

0 < r⁻¹ ↔ 0 < r

theorem nnreal.div_pos {r p : ℝ≥0} (hr : 0 < r) (hp : 0 < p) :

0 < r / p

@[protected]

theorem nnreal.mul_inv {r p : ℝ≥0} :

(r * p)⁻¹ = p⁻¹ * r⁻¹

theorem nnreal.div_self_le (r : ℝ≥0) :

r / r ≤ 1

@[simp]

theorem nnreal.inv_le {r p : ℝ≥0} (h : r ≠ 0) :

r⁻¹ ≤ p ↔ 1 ≤ r * p

theorem nnreal.inv_le_of_le_mul {r p : ℝ≥0} (h : 1 ≤ r * p) :

@[simp]

theorem nnreal.le_inv_iff_mul_le {r p : ℝ≥0} (h : p ≠ 0) :

r ≤ p⁻¹ ↔ r * p ≤ 1

@[simp]

theorem nnreal.lt_inv_iff_mul_lt {r p : ℝ≥0} (h : p ≠ 0) :

r < p⁻¹ ↔ r * p < 1

theorem nnreal.mul_le_iff_le_inv {a b r : ℝ≥0} (hr : r ≠ 0) :

r * a ≤ b ↔ a ≤ r⁻¹ * b

theorem nnreal.le_div_iff_mul_le {a b r : ℝ≥0} (hr : r ≠ 0) :

a ≤ b / r ↔ a * r ≤ b

theorem nnreal.div_le_iff {a b r : ℝ≥0} (hr : r ≠ 0) :

a / r ≤ b ↔ a ≤ b * r

theorem nnreal.div_le_iff' {a b r : ℝ≥0} (hr : r ≠ 0) :

a / r ≤ b ↔ a ≤ r * b

theorem nnreal.div_le_of_le_mul {a b c : ℝ≥0} (h : a ≤ b * c) :

a / c ≤ b

theorem nnreal.div_le_of_le_mul' {a b c : ℝ≥0} (h : a ≤ b * c) :

a / b ≤ c

theorem nnreal.le_div_iff {a b r : ℝ≥0} (hr : r ≠ 0) :

a ≤ b / r ↔ a * r ≤ b

theorem nnreal.le_div_iff' {a b r : ℝ≥0} (hr : r ≠ 0) :

a ≤ b / r ↔ r * a ≤ b

theorem nnreal.div_lt_iff {a b r : ℝ≥0} (hr : r ≠ 0) :

a / r < b ↔ a < b * r

theorem nnreal.div_lt_iff' {a b r : ℝ≥0} (hr : r ≠ 0) :

a / r < b ↔ a < r * b

theorem nnreal.lt_div_iff {a b r : ℝ≥0} (hr : r ≠ 0) :

a < b / r ↔ a * r < b

theorem nnreal.lt_div_iff' {a b r : ℝ≥0} (hr : r ≠ 0) :

a < b / r ↔ r * a < b

theorem nnreal.mul_lt_of_lt_div {a b r : ℝ≥0} (h : a < b / r) :

a * r < b

theorem nnreal.div_le_div_left_of_le {a b c : ℝ≥0} (b0 : 0 < b) (c0 : 0 < c) (cb : c ≤ b) :

a / b ≤ a / c

theorem nnreal.div_le_div_left {a b c : ℝ≥0} (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 : ℝ≥0} (h : ∀ (a : ℝ≥0), a < 1 → a * x ≤ y) :

x ≤ y

theorem nnreal.div_add_div_same (a b c : ℝ≥0) :

a / c + b / c = (a + b) / c

theorem nnreal.half_pos {a : ℝ≥0} (h : 0 < a) :

0 < a / 2

theorem nnreal.add_halves (a : ℝ≥0) :

a / 2 + a / 2 = a

theorem nnreal.half_lt_self {a : ℝ≥0} (h : a ≠ 0) :

a / 2 < a

theorem nnreal.two_inv_lt_one :

theorem nnreal.div_lt_one_of_lt {a b : ℝ≥0} (h : a < b) :

a / b < 1

theorem nnreal.div_add_div (a : ℝ≥0) {b : ℝ≥0} (c : ℝ≥0) {d : ℝ≥0} (hb : b ≠ 0) (hd : d ≠ 0) :

a / b + c / d = (a * d + b * c) / b * d

theorem nnreal.add_div' (a b c : ℝ≥0) (hc : c ≠ 0) :

b + a / c = (b * c + a) / c

theorem nnreal.div_add' (a b c : ℝ≥0) (hc : c ≠ 0) :

a / c + b = (a + b * c) / c

theorem real.to_nnreal_inv {x : ℝ} :

x⁻¹.to_nnreal = (x.to_nnreal)⁻¹

theorem real.to_nnreal_div {x y : ℝ} (hx : 0 ≤ x) :

(x / y).to_nnreal = x.to_nnreal / y.to_nnreal

theorem real.to_nnreal_div' {x y : ℝ} (hy : 0 ≤ y) :

(x / y).to_nnreal = x.to_nnreal / y.to_nnreal

theorem nnreal.inv_lt_one_iff {x : ℝ≥0} (hx : x ≠ 0) :

x⁻¹ < 1 ↔ 1 < x

theorem nnreal.inv_lt_one {x : ℝ≥0} (hx : 1 < x) :

theorem nnreal.zpow_pos {x : ℝ≥0} (hx : x ≠ 0) (n : ℤ) :

0 < x ^ n

theorem nnreal.inv_lt_inv_iff {x y : ℝ≥0} (hx : x ≠ 0) (hy : y ≠ 0) :

y⁻¹ < x⁻¹ ↔ x < y

theorem nnreal.inv_lt_inv {x y : ℝ≥0} (hx : x ≠ 0) (h : x < y) :

y⁻¹ < x⁻¹

@[simp]

theorem nnreal.abs_eq (x : ℝ≥0) :

noncomputable def real.nnabs :

ℝ →*₀ ℝ≥0

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

Equations

real.nnabs = {to_fun := λ (x : ℝ), ⟨|x|, _⟩, map_zero' := real.nnabs._proof_2, map_one' := real.nnabs._proof_3, map_mul' := real.nnabs._proof_4}

@[simp, norm_cast]

theorem real.coe_nnabs (x : ℝ) :

↑(⇑real.nnabs x) = |x|

@[simp]

theorem real.nnabs_of_nonneg {x : ℝ} (h : 0 ≤ x) :

⇑real.nnabs x = x.to_nnreal

theorem real.coe_to_nnreal_le (x : ℝ) :

↑(x.to_nnreal) ≤ |x|

theorem real.cast_nat_abs_eq_nnabs_cast (n : ℤ) :

↑(n.nat_abs) = ⇑real.nnabs ↑n