mathlib3 documentation

data.real.nnreal

Nonnegative real numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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]

def nnreal.strict_ordered_semiring :

strict_ordered_semiring nnreal

@[protected, instance]

noncomputable def nnreal.linear_ordered_semiring :

linear_ordered_semiring nnreal

@[protected, instance]

def nnreal.canonically_ordered_comm_semiring :

canonically_ordered_comm_semiring nnreal

@[protected, instance]

def nnreal.order_bot :

order_bot nnreal

@[protected, instance]

def nnreal.semilattice_inf :

semilattice_inf nnreal

@[protected, instance]

noncomputable def nnreal.floor_semiring :

floor_semiring nnreal

@[protected, instance]

def nnreal.inhabited :

inhabited nnreal

@[protected, instance]

def nnreal.comm_monoid_with_zero :

comm_monoid_with_zero nnreal

@[protected, instance]

def nnreal.distrib_lattice :

distrib_lattice nnreal

@[protected, instance]

def nnreal.archimedean :

archimedean nnreal

@[protected, instance]

def nnreal.ordered_comm_semiring :

ordered_comm_semiring nnreal

@[protected, instance]

noncomputable def nnreal.linear_ordered_comm_group_with_zero :

linear_ordered_comm_group_with_zero nnreal

@[protected, instance]

noncomputable def nnreal.has_sub :

@[protected, instance]

def nnreal.has_ordered_sub :

has_ordered_sub nnreal

@[protected, instance]

def nnreal.comm_semiring :

comm_semiring nnreal

@[protected, instance]

def nnreal.semiring :

semiring nnreal

@[protected, instance]

def nnreal.densely_ordered :

densely_ordered nnreal

def nnreal :

Nonnegative real numbers.

Equations

nnreal = {r // 0 ≤ r}

Instances for nnreal

@[protected, instance]

noncomputable def nnreal.canonically_linear_ordered_semifield :

canonically_linear_ordered_semifield nnreal

@[protected, instance]

noncomputable def nnreal.has_div :

@[protected, instance]

def nnreal.semilattice_sup :

semilattice_sup nnreal

@[protected, instance]

def nnreal.real.has_coe :

has_coe nnreal ℝ

Equations

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

@[simp]

theorem nnreal.val_eq_coe (n : nnreal) :

@[protected, instance]

def nnreal.can_lift :

can_lift ℝ nnreal coe (λ (r : ℝ), 0 ≤ r)

Equations

nnreal.can_lift = subtype.can_lift (λ (r : ℝ), 0 ≤ r)

@[protected]

theorem nnreal.eq {n m : nnreal} :

↑n = ↑m → n = 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

r.to_nnreal = ⟨linear_order.max r 0, _⟩

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

↑(r.to_nnreal) = r

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

r.to_nnreal = ⟨r, hr⟩

theorem real.le_coe_to_nnreal (r : ℝ) :

r ≤ ↑(r.to_nnreal)

theorem nnreal.coe_nonneg (r : nnreal) :

@[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₂ : 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) :

↑r⁻¹ = (↑r)⁻¹

@[protected]

theorem nnreal.coe_div (r₁ r₂ : nnreal) :

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

@[protected, simp, norm_cast]

theorem nnreal.coe_bit0 (r : nnreal) :

↑(bit0 r) = bit0 ↑r

@[protected, simp, norm_cast]

theorem nnreal.coe_bit1 (r : nnreal) :

↑(bit1 r) = 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

def nnreal.to_real_hom :

nnreal →+* ℝ

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 nnreal 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 : nnreal) (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_smul M N] [is_scalar_tower ℝ M N] :

is_scalar_tower nnreal M N

@[protected, instance]

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

smul_comm_class nnreal M N

@[protected, instance]

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

smul_comm_class M nnreal N

@[protected, instance]

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

distrib_mul_action nnreal 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 nnreal 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 nnreal A

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

Equations

nnreal.algebra = {to_has_smul := {smul := has_smul.smul smul_zero_class.to_has_smul}, 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 : α → 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) = (list.map coe l).sum

@[norm_cast]

theorem nnreal.coe_list_prod (l : list nnreal) :

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

@[norm_cast]

theorem nnreal.coe_multiset_sum (s : multiset nnreal) :

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

@[norm_cast]

theorem nnreal.coe_multiset_prod (s : multiset nnreal) :

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

@[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 ∈ s → 0 ≤ 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 ∈ s → 0 ≤ 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]

theorem real.to_nnreal_mono :

monotone real.to_nnreal

@[simp]

theorem real.to_nnreal_coe {r : nnreal} :

↑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

@[simp]

theorem nnreal.order_iso_Icc_zero_coe_apply_coe_coe (a : nnreal) (ᾰ : {x // set.Ici 0 x ∧ (λ (x : ℝ), x ≤ ↑a) x}) :

↑↑(⇑(a.order_iso_Icc_zero_coe) ᾰ) = ↑ᾰ

def nnreal.order_iso_Icc_zero_coe (a : nnreal) :

↥(set.Icc 0 ↑a) ≃o ↥(set.Iic a)

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

Equations

a.order_iso_Icc_zero_coe = {to_equiv := equiv.set.sep (set.Ici 0) (λ (x : ℝ), x ≤ ↑a), map_rel_iff' := _}

@[simp]

theorem nnreal.order_iso_Icc_zero_coe_symm_apply_coe (a : nnreal) (b : ↥(set.Iic a)) :

↑(⇑(a.order_iso_Icc_zero_coe.symm) b) = ↑b

theorem nnreal.coe_image {s : set nnreal} :

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

theorem nnreal.bdd_above_coe {s : set nnreal} :

bdd_above (coe '' s) ↔ bdd_above s

theorem nnreal.bdd_below_coe (s : set nnreal) :

bdd_below (coe '' s)

@[protected, instance]

noncomputable def nnreal.conditionally_complete_linear_order_bot :

conditionally_complete_linear_order_bot nnreal

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 nnreal) :

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

@[norm_cast]

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

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

@[norm_cast]

theorem nnreal.coe_Inf (s : set nnreal) :

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

@[simp]

theorem nnreal.Inf_empty :

has_Inf.Inf ∅ = 0

@[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]

def nnreal.covariant_add :

covariant_class nnreal nnreal has_add.add has_le.le

@[protected, instance]

def nnreal.contravariant_add :

contravariant_class nnreal nnreal has_add.add has_lt.lt

@[protected, instance]

def nnreal.covariant_mul :

covariant_class nnreal nnreal has_mul.mul has_le.le

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 :

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

↑(linear_order.max x y) = linear_order.max ↑x ↑y

@[simp, norm_cast]

theorem nnreal.coe_min (x y : nnreal) :

↑(linear_order.min x y) = linear_order.min ↑x ↑y

@[simp]

theorem nnreal.zero_le_coe {q : nnreal} :

@[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) = linear_order.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_eq_to_nnreal_iff {r p : ℝ} (hr : 0 ≤ r) (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 : nnreal} :

r.to_nnreal ≤ p ↔ r ≤ ↑p

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

r ≤ p.to_nnreal ↔ ↑r ≤ p

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

r ≤ p.to_nnreal ↔ ↑r ≤ p

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

r.to_nnreal < p ↔ r < ↑p

theorem real.lt_to_nnreal_iff_coe_lt {r : nnreal} {p : ℝ} :

r < p.to_nnreal ↔ ↑r < p

@[simp]

theorem real.to_nnreal_bit0 (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 real.to_nnreal_pow {x : ℝ} (hx : 0 ≤ x) (n : ℕ) :

(x ^ n).to_nnreal = x.to_nnreal ^ n

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 = p.to_nnreal * 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))

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 : nnreal} :

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

theorem nnreal.coe_sub_def {r p : nnreal} :

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

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_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 < 1 → a * 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 b : nnreal} (h : a < b) :

a / b < 1

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 : 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 y : nnreal} (hx : x ≠ 0) (h : x < y) :

y⁻¹ < x⁻¹

@[simp]

theorem nnreal.abs_eq (x : nnreal) :

theorem nnreal.le_to_nnreal_of_coe_le {x : nnreal} {y : ℝ} (h : ↑x ≤ y) :

x ≤ y.to_nnreal

theorem nnreal.Sup_of_not_bdd_above {s : set nnreal} (hs : ¬bdd_above s) :

has_Sup.Sup s = 0

theorem nnreal.supr_of_not_bdd_above {ι : Sort u_1} {f : ι → nnreal} (hf : ¬bdd_above (set.range f)) :

(⨆ (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

theorem set.ord_connected.preimage_coe_nnreal_real {s : set ℝ} (h : s.ord_connected) :

(coe ⁻¹' s).ord_connected

theorem set.ord_connected.image_coe_nnreal_real {t : set nnreal} (h : t.ord_connected) :

(coe '' t).ord_connected

theorem set.ord_connected.image_real_to_nnreal {s : set ℝ} (h : s.ord_connected) :

(real.to_nnreal '' s).ord_connected

theorem set.ord_connected.preimage_real_to_nnreal {t : set nnreal} (h : t.ord_connected) :

(real.to_nnreal ⁻¹' t).ord_connected

def real.nnabs :

ℝ →*₀ nnreal

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.nnabs_coe (x : nnreal) :

⇑real.nnabs ↑x = x

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

meta def tactic.positivity_coe_nnreal_real :

expr → tactic tactic.positivity.strictness

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