Documentation

Mathlib.Data.NNReal.Defs

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;
- CanonicallyOrderedAdd ℝ≥0;
- LinearOrderedCommGroupWithZero ℝ≥0;
- CanonicallyLinearOrderedAddCommMonoid ℝ≥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.lean.
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.

def NNReal :

Nonnegative real numbers, denoted as ℝ≥0 within the NNReal namespace

Equations

NNReal = { r : ℝ // 0 ≤ r }

instance instNNRealZero :

Equations

instNNRealZero = Nonneg.zero

instance instNNRealOne :

Equations

instNNRealOne = Nonneg.one

instance instNNRealSemiring :

Semiring NNReal

Equations

instNNRealSemiring = Nonneg.semiring

instance instNNRealCommMonoidWithZero :

CommMonoidWithZero NNReal

Equations

instNNRealCommMonoidWithZero = Nonneg.commMonoidWithZero

instance instNNRealCommSemiring :

CommSemiring NNReal

Equations

instNNRealCommSemiring = Nonneg.commSemiring

instance instNNRealPartialOrder :

PartialOrder NNReal

Equations

instNNRealPartialOrder = Subtype.partialOrder fun (r : ℝ) => 0 ≤ r

instance instNNRealSemilatticeInf :

SemilatticeInf NNReal

Equations

instNNRealSemilatticeInf = Nonneg.semilatticeInf

instance instNNRealSemilatticeSup :

SemilatticeSup NNReal

Equations

instNNRealSemilatticeSup = Nonneg.semilatticeSup

instance instNNRealDistribLattice :

DistribLattice NNReal

Equations

instNNRealDistribLattice = Nonneg.distribLattice

instance instNNRealNontrivial :

Nontrivial NNReal

Equations

instNNRealNontrivial = ⋯

instance instNNRealInhabited :

Inhabited NNReal

Equations

instNNRealInhabited = Nonneg.inhabited

def NNReal.«termℝ≥0» :

Lean.ParserDescr

Nonnegative real numbers, denoted as ℝ≥0 within the NNReal namespace

Equations

NNReal.«termℝ≥0» = Lean.ParserDescr.node `NNReal.«termℝ≥0» 1024 (Lean.ParserDescr.symbol "ℝ≥0")

instance NNReal.instCanonicallyOrderedAdd :

CanonicallyOrderedAdd NNReal

instance NNReal.instNoZeroDivisors :

NoZeroDivisors NNReal

instance NNReal.instDenselyOrdered :

DenselyOrdered NNReal

instance NNReal.instOrderBot :

OrderBot NNReal

Equations

NNReal.instOrderBot = Nonneg.orderBot

instance NNReal.instArchimedean :

Archimedean NNReal

instance NNReal.instMulArchimedean :

MulArchimedean NNReal

instance NNReal.instMin :

Equations

NNReal.instMin = SemilatticeInf.toMin

instance NNReal.instMax :

Equations

NNReal.instMax = SemilatticeSup.toMax

instance NNReal.instSub :

Equations

NNReal.instSub = Nonneg.sub

instance NNReal.instOrderedSub :

OrderedSub NNReal

instance NNReal.instNNRatCast :

NNRatCast NNReal

Equations

NNReal.instNNRatCast = { nnratCast := fun (r : ℚ≥0) => ⟨↑r, ⋯⟩ }

noncomputable instance NNReal.instLinearOrder :

LinearOrder NNReal

Equations

NNReal.instLinearOrder = Subtype.instLinearOrder fun (r : ℝ) => 0 ≤ r

noncomputable instance NNReal.instSemifield :

Semifield NNReal

Equations

NNReal.instSemifield = Nonneg.semifield

instance NNReal.instIsOrderedRing :

IsOrderedRing NNReal

instance NNReal.instIsStrictOrderedRing :

IsStrictOrderedRing NNReal

noncomputable instance NNReal.instLinearOrderedCommGroupWithZero :

LinearOrderedCommGroupWithZero NNReal

Equations

NNReal.instLinearOrderedCommGroupWithZero = Nonneg.linearOrderedCommGroupWithZero

def NNReal.toReal :

Coercion ℝ≥0 → ℝ.

Equations

NNReal.toReal = Subtype.val

instance NNReal.instCoeReal :

Equations

NNReal.instCoeReal = { coe := NNReal.toReal }

@[simp]

theorem NNReal.val_eq_coe (n : NNReal) :

↑n = ↑n

instance NNReal.canLift :

CanLift ℝ NNReal toReal fun (r : ℝ) => 0 ≤ r

theorem NNReal.eq {n m : NNReal} :

↑n = ↑m → n = m

theorem NNReal.eq_iff {n m : NNReal} :

n = m ↔ ↑n = ↑m

theorem NNReal.ne_iff {x y : NNReal} :

↑x ≠ ↑y ↔ x ≠ y

theorem NNReal.forall {p : NNReal → Prop} :

(∀ (x : NNReal), p x) ↔ ∀ (x : ℝ) (hx : 0 ≤ x), p ⟨x, hx⟩

theorem NNReal.exists {p : NNReal → Prop} :

(∃ (x : NNReal), p x) ↔ ∃ (x : ℝ) (hx : 0 ≤ x), p ⟨x, hx⟩

def Real.toNNReal (r : ℝ) :

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

Equations

r.toNNReal = ⟨max r 0, ⋯⟩

theorem Real.coe_toNNReal (r : ℝ) (hr : 0 ≤ r) :

↑r.toNNReal = r

theorem Real.toNNReal_of_nonneg {r : ℝ} (hr : 0 ≤ r) :

r.toNNReal = ⟨r, hr⟩

theorem Real.le_coe_toNNReal (r : ℝ) :

r ≤ ↑r.toNNReal

theorem NNReal.coe_nonneg (r : NNReal) :

0 ≤ ↑r

@[simp]

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

↑⟨a, ha⟩ = a

theorem NNReal.coe_injective :

Function.Injective toReal

@[simp]

theorem NNReal.coe_inj {r₁ r₂ : NNReal} :

↑r₁ = ↑r₂ ↔ r₁ = r₂

@[simp]

theorem NNReal.coe_zero :

↑0 = 0

@[simp]

theorem NNReal.coe_one :

↑1 = 1

@[simp]

theorem NNReal.mk_zero :

⟨0, ⋯⟩ = 0

@[simp]

theorem NNReal.mk_one :

⟨1, ⋯⟩ = 1

@[simp]

theorem NNReal.coe_add (r₁ r₂ : NNReal) :

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

@[simp]

theorem NNReal.coe_mul (r₁ r₂ : NNReal) :

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

@[simp]

theorem NNReal.coe_inv (r : NNReal) :

↑r⁻¹ = (↑r)⁻¹

@[simp]

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

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

theorem NNReal.coe_two :

↑2 = 2

@[simp]

theorem NNReal.coe_sub {r₁ 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

theorem NNReal.coe_ne_one {r : NNReal} :

↑r ≠ 1 ↔ r ≠ 1

def NNReal.toRealHom :

NNReal →+* ℝ

Coercion ℝ≥0 → ℝ as a RingHom.

TODO: what if we define Coe ℝ≥0 ℝ using this function?

Equations

NNReal.toRealHom = { toFun := NNReal.toReal, map_one' := NNReal.coe_one, map_mul' := NNReal.coe_mul, map_zero' := NNReal.coe_zero, map_add' := NNReal.coe_add }

@[simp]

theorem NNReal.coe_toRealHom :

⇑toRealHom = toReal

instance NNReal.instMulActionOfReal {M : Type u_1} [MulAction ℝ M] :

MulAction NNReal M

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

Equations

NNReal.instMulActionOfReal = MulAction.compHom M ↑NNReal.toRealHom

theorem NNReal.smul_def {M : Type u_1} [MulAction ℝ M] (c : NNReal) (x : M) :

c • x = ↑c • x

instance NNReal.instIsScalarTowerOfReal {M : Type u_1} {N : Type u_2} [MulAction ℝ M] [MulAction ℝ N] [SMul M N] [IsScalarTower ℝ M N] :

IsScalarTower NNReal M N

instance NNReal.smulCommClass_left {M : Type u_1} {N : Type u_2} [MulAction ℝ N] [SMul M N] [SMulCommClass ℝ M N] :

SMulCommClass NNReal M N

instance NNReal.smulCommClass_right {M : Type u_1} {N : Type u_2} [MulAction ℝ N] [SMul M N] [SMulCommClass M ℝ N] :

SMulCommClass M NNReal N

instance NNReal.instDistribMulActionOfReal {M : Type u_1} [AddMonoid M] [DistribMulAction ℝ M] :

DistribMulAction NNReal M

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

Equations

NNReal.instDistribMulActionOfReal = DistribMulAction.compHom M ↑NNReal.toRealHom

instance NNReal.instModuleOfReal {M : Type u_1} [AddCommMonoid M] [Module ℝ M] :

Module NNReal M

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

Equations

NNReal.instModuleOfReal = Module.compHom M NNReal.toRealHom

instance NNReal.instAlgebraOfReal {A : Type u_1} [Semiring A] [Algebra ℝ A] :

Algebra NNReal A

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

Equations

NNReal.instAlgebraOfReal = { smul := fun (x1 : NNReal) (x2 : A) => x1 • x2, algebraMap := (algebraMap ℝ A).comp NNReal.toRealHom, commutes' := ⋯, smul_def' := ⋯ }

@[simp]

theorem NNReal.coe_pow (r : NNReal) (n : ℕ) :

↑(r ^ n) = ↑r ^ n

@[simp]

theorem NNReal.coe_zpow (r : NNReal) (n : ℤ) :

↑(r ^ n) = ↑r ^ n

@[simp]

theorem NNReal.coe_nsmul (r : NNReal) (n : ℕ) :

↑(n • r) = n • ↑r

@[simp]

theorem NNReal.coe_nnqsmul (q : ℚ≥0) (x : NNReal) :

↑(q • x) = q • ↑x

@[simp]

theorem NNReal.coe_natCast (n : ℕ) :

↑↑n = ↑n

@[simp]

theorem NNReal.coe_ofNat (n : ℕ) [n.AtLeastTwo] :

↑(OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem NNReal.coe_ofScientific (m : ℕ) (s : Bool) (e : ℕ) :

↑(OfScientific.ofScientific m s e) = OfScientific.ofScientific m s e

@[simp]

theorem NNReal.algebraMap_eq_coe :

⇑(algebraMap NNReal ℝ) = toReal

@[simp]

theorem NNReal.coe_le_coe {r₁ r₂ : NNReal} :

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

@[simp]

theorem NNReal.coe_lt_coe {r₁ r₂ : NNReal} :

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

@[simp]

theorem NNReal.coe_pos {r : NNReal} :

0 < ↑r ↔ 0 < r

@[simp]

theorem NNReal.one_le_coe {r : NNReal} :

1 ≤ ↑r ↔ 1 ≤ r

@[simp]

theorem NNReal.one_lt_coe {r : NNReal} :

1 < ↑r ↔ 1 < r

@[simp]

theorem NNReal.coe_le_one {r : NNReal} :

↑r ≤ 1 ↔ r ≤ 1

@[simp]

theorem NNReal.coe_lt_one {r : NNReal} :

↑r < 1 ↔ r < 1

theorem NNReal.coe_mono :

Monotone toReal

theorem NNReal.GCongr.toReal_le_toReal {r₁ r₂ : NNReal} :

r₁ ≤ r₂ → ↑r₁ ≤ ↑r₂

Alias for the use of gcongr

theorem Real.toNNReal_mono :

Monotone toNNReal

@[simp]

theorem Real.toNNReal_coe {r : NNReal} :

(↑r).toNNReal = r

@[simp]

theorem NNReal.mk_natCast (n : ℕ) :

⟨↑n, ⋯⟩ = ↑n

@[simp]

theorem Real.toNNReal_coe_nat (n : ℕ) :

(↑n).toNNReal = ↑n

@[deprecated Real.toNNReal_coe_nat (since := "2025-03-12")]

theorem NNReal.toNNReal_coe_nat (n : ℕ) :

(↑n).toNNReal = ↑n

Alias of Real.toNNReal_coe_nat.

@[simp]

theorem Real.toNNReal_ofNat (n : ℕ) [n.AtLeastTwo] :

(OfNat.ofNat n).toNNReal = OfNat.ofNat n

def NNReal.gi :

GaloisInsertion Real.toNNReal toReal

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

Equations

NNReal.gi = GaloisInsertion.monotoneIntro NNReal.coe_mono Real.toNNReal_mono Real.le_coe_toNNReal ⋯

instance NNReal.instPosSMulStrictMono {α : Type u_2} [Preorder α] [MulAction ℝ α] [PosSMulStrictMono ℝ α] :

PosSMulStrictMono NNReal α

instance NNReal.instSMulPosStrictMono {α : Type u_2} [Zero α] [Preorder α] [MulAction ℝ α] [SMulPosStrictMono ℝ α] :

SMulPosStrictMono NNReal α

def NNReal.orderIsoIccZeroCoe (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.orderIsoIccZeroCoe = { toEquiv := Equiv.Set.sep (Set.Ici 0) fun (x : ℝ) => x ≤ ↑a, map_rel_iff' := ⋯ }

@[simp]

theorem NNReal.orderIsoIccZeroCoe_apply_coe_coe (a : NNReal) (b : ↑(Set.Icc 0 ↑a)) :

↑↑(a.orderIsoIccZeroCoe b) = ↑b

@[simp]

theorem NNReal.orderIsoIccZeroCoe_symm_apply_coe (a : NNReal) (b : ↑(Set.Iic a)) :

↑(a.orderIsoIccZeroCoe.symm b) = ↑↑b

theorem NNReal.coe_image {s : Set NNReal} :

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

theorem NNReal.bddAbove_coe {s : Set NNReal} :

BddAbove (toReal '' s) ↔ BddAbove s

theorem NNReal.bddBelow_coe (s : Set NNReal) :

BddBelow (toReal '' s)

noncomputable instance NNReal.instConditionallyCompleteLinearOrderBot :

ConditionallyCompleteLinearOrderBot NNReal

Equations

NNReal.instConditionallyCompleteLinearOrderBot = Nonneg.conditionallyCompleteLinearOrderBot 0

theorem NNReal.coe_sSup (s : Set NNReal) :

↑(sSup s) = sSup (toReal '' s)

@[simp]

theorem NNReal.coe_iSup {ι : Sort u_2} (s : ι → NNReal) :

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

theorem NNReal.coe_sInf (s : Set NNReal) :

↑(sInf s) = sInf (toReal '' s)

@[simp]

theorem NNReal.sInf_empty :

theorem NNReal.coe_iInf {ι : Sort u_2} (s : ι → NNReal) :

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

instance NNReal.addLeftMono :

AddLeftMono NNReal

instance NNReal.addLeftReflectLT :

AddLeftReflectLT NNReal

instance NNReal.mulLeftMono :

MulLeftMono NNReal

theorem NNReal.lt_iff_exists_rat_btwn (a b : NNReal) :

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

theorem NNReal.bot_eq_zero :

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

a * max b c = max (a * b) (a * c)

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

max a b * c = max (a * c) (b * c)

@[simp]

theorem NNReal.coe_max (x y : NNReal) :

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

@[simp]

theorem NNReal.coe_min (x y : NNReal) :

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

@[simp]

theorem NNReal.zero_le_coe {q : NNReal} :

0 ≤ ↑q

instance NNReal.instOrderedSMul {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [Module ℝ M] [OrderedSMul ℝ M] :

OrderedSMul NNReal M

@[simp]

theorem Real.coe_toNNReal' (r : ℝ) :

↑r.toNNReal = max r 0

@[simp]

theorem Real.toNNReal_zero :

@[simp]

theorem Real.toNNReal_one :

@[simp]

theorem Real.toNNReal_pos {r : ℝ} :

0 < r.toNNReal ↔ 0 < r

@[simp]

theorem Real.toNNReal_eq_zero {r : ℝ} :

r.toNNReal = 0 ↔ r ≤ 0

theorem Real.toNNReal_of_nonpos {r : ℝ} :

r ≤ 0 → r.toNNReal = 0

theorem Real.toNNReal_eq_iff_eq_coe {r : ℝ} {p : NNReal} (hp : p ≠ 0) :

r.toNNReal = p ↔ r = ↑p

@[simp]

theorem Real.toNNReal_eq_one {r : ℝ} :

r.toNNReal = 1 ↔ r = 1

@[simp]

theorem Real.toNNReal_eq_natCast {r : ℝ} {n : ℕ} (hn : n ≠ 0) :

r.toNNReal = ↑n ↔ r = ↑n

@[simp]

theorem Real.toNNReal_eq_ofNat {r : ℝ} {n : ℕ} [n.AtLeastTwo] :

r.toNNReal = OfNat.ofNat n ↔ r = OfNat.ofNat n

@[simp]

theorem Real.toNNReal_le_toNNReal_iff {r p : ℝ} (hp : 0 ≤ p) :

r.toNNReal ≤ p.toNNReal ↔ r ≤ p

@[simp]

theorem Real.toNNReal_le_one {r : ℝ} :

r.toNNReal ≤ 1 ↔ r ≤ 1

@[simp]

theorem Real.one_lt_toNNReal {r : ℝ} :

1 < r.toNNReal ↔ 1 < r

@[simp]

theorem Real.toNNReal_le_natCast {r : ℝ} {n : ℕ} :

r.toNNReal ≤ ↑n ↔ r ≤ ↑n

@[simp]

theorem Real.natCast_lt_toNNReal {r : ℝ} {n : ℕ} :

↑n < r.toNNReal ↔ ↑n < r

@[simp]

theorem Real.toNNReal_le_ofNat {r : ℝ} {n : ℕ} [n.AtLeastTwo] :

r.toNNReal ≤ OfNat.ofNat n ↔ r ≤ ↑n

@[simp]

theorem Real.ofNat_lt_toNNReal {r : ℝ} {n : ℕ} [n.AtLeastTwo] :

OfNat.ofNat n < r.toNNReal ↔ ↑n < r

@[simp]

theorem Real.toNNReal_eq_toNNReal_iff {r p : ℝ} (hr : 0 ≤ r) (hp : 0 ≤ p) :

r.toNNReal = p.toNNReal ↔ r = p

@[simp]

theorem Real.toNNReal_lt_toNNReal_iff' {r p : ℝ} :

r.toNNReal < p.toNNReal ↔ r < p ∧ 0 < p

theorem Real.toNNReal_lt_toNNReal_iff {r p : ℝ} (h : 0 < p) :

r.toNNReal < p.toNNReal ↔ r < p

theorem Real.lt_of_toNNReal_lt {r p : ℝ} (h : r.toNNReal < p.toNNReal) :

r < p

theorem Real.toNNReal_lt_toNNReal_iff_of_nonneg {r p : ℝ} (hr : 0 ≤ r) :

r.toNNReal < p.toNNReal ↔ r < p

theorem Real.toNNReal_le_toNNReal_iff' {r p : ℝ} :

r.toNNReal ≤ p.toNNReal ↔ r ≤ p ∨ r ≤ 0

theorem Real.toNNReal_le_toNNReal_iff_of_pos {r p : ℝ} (hr : 0 < r) :

r.toNNReal ≤ p.toNNReal ↔ r ≤ p

@[simp]

theorem Real.one_le_toNNReal {r : ℝ} :

1 ≤ r.toNNReal ↔ 1 ≤ r

@[simp]

theorem Real.toNNReal_lt_one {r : ℝ} :

r.toNNReal < 1 ↔ r < 1

@[simp]

theorem Real.natCastle_toNNReal' {n : ℕ} {r : ℝ} :

↑n ≤ r.toNNReal ↔ ↑n ≤ r ∨ n = 0

@[simp]

theorem Real.toNNReal_lt_natCast' {n : ℕ} {r : ℝ} :

r.toNNReal < ↑n ↔ r < ↑n ∧ n ≠ 0

theorem Real.natCast_le_toNNReal {n : ℕ} {r : ℝ} (hn : n ≠ 0) :

↑n ≤ r.toNNReal ↔ ↑n ≤ r

theorem Real.toNNReal_lt_natCast {r : ℝ} {n : ℕ} (hn : n ≠ 0) :

r.toNNReal < ↑n ↔ r < ↑n

@[simp]

theorem Real.toNNReal_lt_ofNat {r : ℝ} {n : ℕ} [n.AtLeastTwo] :

r.toNNReal < OfNat.ofNat n ↔ r < OfNat.ofNat n

@[simp]

theorem Real.ofNat_le_toNNReal {n : ℕ} {r : ℝ} [n.AtLeastTwo] :

OfNat.ofNat n ≤ r.toNNReal ↔ OfNat.ofNat n ≤ r

@[simp]

theorem Real.toNNReal_add {r p : ℝ} (hr : 0 ≤ r) (hp : 0 ≤ p) :

(r + p).toNNReal = r.toNNReal + p.toNNReal

theorem Real.toNNReal_add_toNNReal {r p : ℝ} (hr : 0 ≤ r) (hp : 0 ≤ p) :

r.toNNReal + p.toNNReal = (r + p).toNNReal

theorem Real.toNNReal_le_toNNReal {r p : ℝ} (h : r ≤ p) :

r.toNNReal ≤ p.toNNReal

theorem Real.toNNReal_add_le {r p : ℝ} :

(r + p).toNNReal ≤ r.toNNReal + p.toNNReal

theorem Real.toNNReal_le_iff_le_coe {r : ℝ} {p : NNReal} :

r.toNNReal ≤ p ↔ r ≤ ↑p

theorem Real.le_toNNReal_iff_coe_le {r : NNReal} {p : ℝ} (hp : 0 ≤ p) :

r ≤ p.toNNReal ↔ ↑r ≤ p

theorem Real.le_toNNReal_iff_coe_le' {r : NNReal} {p : ℝ} (hr : 0 < r) :

r ≤ p.toNNReal ↔ ↑r ≤ p

theorem Real.toNNReal_lt_iff_lt_coe {r : ℝ} {p : NNReal} (ha : 0 ≤ r) :

r.toNNReal < p ↔ r < ↑p

theorem Real.lt_toNNReal_iff_coe_lt {r : NNReal} {p : ℝ} :

r < p.toNNReal ↔ ↑r < p

theorem Real.toNNReal_pow {x : ℝ} (hx : 0 ≤ x) (n : ℕ) :

(x ^ n).toNNReal = x.toNNReal ^ n

theorem Real.toNNReal_zpow {x : ℝ} (hx : 0 ≤ x) (n : ℤ) :

(x ^ n).toNNReal = x.toNNReal ^ n

theorem Real.toNNReal_mul {p q : ℝ} (hp : 0 ≤ p) :

(p * q).toNNReal = p.toNNReal * q.toNNReal

theorem NNReal.mul_eq_mul_left {a b 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 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 OrderedSub in the file Mathlib/Algebra/Order/Sub/Basic.lean. See also mul_tsub and tsub_mul.

theorem NNReal.sub_def {r p : NNReal} :

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

theorem NNReal.coe_sub_def {r p : NNReal} :

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

@[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.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.mul_lt_of_lt_div {a b r : NNReal} (h : a < b / r) :

a * r < b

@[deprecated div_le_div_of_nonneg_left (since := "2024-11-12")]

theorem NNReal.div_le_div_left_of_le {a b c : NNReal} (c0 : c ≠ 0) (cb : c ≤ b) :

a / b ≤ a / c

@[deprecated div_le_div_iff_of_pos_left (since := "2024-11-12")]

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 < 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.toNNReal_inv {x : ℝ} :

x⁻¹.toNNReal = x.toNNReal⁻¹

theorem Real.toNNReal_div {x y : ℝ} (hx : 0 ≤ x) :

(x / y).toNNReal = x.toNNReal / y.toNNReal

theorem Real.toNNReal_div' {x y : ℝ} (hy : 0 ≤ y) :

(x / y).toNNReal = x.toNNReal / y.toNNReal

theorem NNReal.inv_lt_one_iff {x : NNReal} (hx : x ≠ 0) :

x⁻¹ < 1 ↔ 1 < x

theorem NNReal.inv_lt_inv {x y : NNReal} (hx : x ≠ 0) (h : x < y) :

y⁻¹ < x⁻¹

theorem NNReal.exists_nat_pos_inv_lt {b : NNReal} (hb : 0 < b) :

∃ (n : ℕ), 0 < n ∧ (↑n)⁻¹ < b

@[simp]

theorem NNReal.abs_eq (x : NNReal) :

|↑x| = ↑x

theorem NNReal.le_toNNReal_of_coe_le {x : NNReal} {y : ℝ} (h : ↑x ≤ y) :

x ≤ y.toNNReal

theorem NNReal.sSup_of_not_bddAbove {s : Set NNReal} (hs : ¬BddAbove s) :

sSup s = 0

theorem NNReal.iSup_of_not_bddAbove {ι : Sort u_1} {f : ι → NNReal} (hf : ¬BddAbove (Set.range f)) :

⨆ (i : ι), f i = 0

theorem NNReal.iSup_empty {ι : Sort u_1} [IsEmpty ι] (f : ι → NNReal) :

⨆ (i : ι), f i = 0

theorem NNReal.iInf_empty {ι : Sort u_1} [IsEmpty ι] (f : ι → NNReal) :

⨅ (i : ι), f i = 0

@[simp]

theorem NNReal.iSup_eq_zero {ι : Sort u_1} {f : ι → NNReal} (hf : BddAbove (Set.range f)) :

⨆ (i : ι), f i = 0 ↔ ∀ (i : ι), f i = 0

@[simp]

theorem NNReal.iInf_const_zero {α : Sort u_2} :

⨅ (x : α), 0 = 0

theorem Set.OrdConnected.preimage_coe_nnreal_real {s : Set ℝ} (h : s.OrdConnected) :

(NNReal.toReal ⁻¹' s).OrdConnected

theorem Set.OrdConnected.image_coe_nnreal_real {t : Set NNReal} (h : t.OrdConnected) :

(NNReal.toReal '' t).OrdConnected

theorem Set.OrdConnected.image_real_toNNReal {s : Set ℝ} (h : s.OrdConnected) :

(Real.toNNReal '' s).OrdConnected

theorem Set.OrdConnected.preimage_real_toNNReal {t : Set NNReal} (h : t.OrdConnected) :

(Real.toNNReal ⁻¹' t).OrdConnected

def Real.nnabs :

ℝ →*₀ NNReal

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

Equations

Real.nnabs = { toFun := fun (x : ℝ) => ⟨|x|, ⋯⟩, map_zero' := Real.nnabs._proof_58, map_one' := Real.nnabs._proof_60, map_mul' := Real.nnabs._proof_62 }

@[simp]

theorem Real.coe_nnabs (x : ℝ) :

↑(nnabs x) = |x|

@[simp]

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

nnabs x = x.toNNReal

theorem Real.nnabs_coe (x : NNReal) :

nnabs ↑x = x

theorem Real.coe_toNNReal_le (x : ℝ) :

↑x.toNNReal ≤ |x|

@[simp]

theorem Real.toNNReal_abs (x : ℝ) :

|x|.toNNReal = nnabs x

theorem Real.cast_natAbs_eq_nnabs_cast (n : ℤ) :

↑n.natAbs = nnabs ↑n

theorem Real.nnreal_dichotomy (r : ℝ) :

∃ (x : NNReal), r = ↑x ∨ r = -↑x

Every real number nonnegative or nonpositive, phrased using ℝ≥0.

theorem Real.nnreal_trichotomy (r : ℝ) :

r = 0 ∨ ∃ (x : NNReal), 0 < x ∧ (r = ↑x ∨ r = -↑x)

Every real number is either zero, positive or negative, phrased using ℝ≥0.

theorem Real.nnreal_induction_on {motive : ℝ → Prop} (nonneg : ∀ (x : NNReal), motive ↑x) (nonpos : ∀ (x : NNReal), motive ↑x → motive (-↑x)) (r : ℝ) :

motive r

To prove a property holds for real numbers it suffices to show that it holds for x : ℝ≥0, and if it holds for x : ℝ≥0, then it does also for (-↑x : ℝ).

theorem Real.nnreal_induction_on' {motive : ℝ → Prop} (zero : motive 0) (pos : ∀ (x : NNReal), 0 < x → motive ↑x) (neg : ∀ (x : NNReal), 0 < x → motive ↑x → motive (-↑x)) (r : ℝ) :

motive r

A version of nnreal_induction_on which splits into three cases (zero, positive and negative) instead of two.

theorem NNReal.exists_lt_of_strictMono {Γ₀ : Type u_1} [LinearOrderedCommGroupWithZero Γ₀] [h : Nontrivial Γ₀ˣ] {f : Γ₀ →*₀ NNReal} (hf : StrictMono ⇑f) {r : NNReal} (hr : 0 < r) :

∃ (d : Γ₀ˣ), f ↑d < r

If Γ₀ˣ is nontrivial and f : Γ₀ →*₀ ℝ≥0 is strictly monotone, then for any positive r : ℝ≥0, there exists d : Γ₀ˣ with f d < r.

theorem Real.exists_lt_of_strictMono {Γ₀ : Type u_1} [LinearOrderedCommGroupWithZero Γ₀] [h : Nontrivial Γ₀ˣ] {f : Γ₀ →*₀ NNReal} (hf : StrictMono ⇑f) {r : ℝ} (hr : 0 < r) :

∃ (d : Γ₀ˣ), ↑(f ↑d) < r

If Γ₀ˣ is nontrivial and f : Γ₀ →*₀ ℝ≥0 is strictly monotone, then for any positive real r, there exists d : Γ₀ˣ with f d < r.

unsafe instance instReprNNReal :

While not very useful, this instance uses the same representation as Real.instRepr.

Equations

instReprNNReal = { reprPrec := fun (r : NNReal) (x : ℕ) => Std.format "(" ++ Std.format (repr ↑r) ++ Std.format ").toNNReal" }

def Mathlib.Meta.Positivity.evalNNRealtoReal :

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