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:

  • IsOrderedRing ℝ≥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.

Notation

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

def NNReal : Type

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

def NNReal.«termℝ≥0» : Lean.ParserDescr

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

def NNReal.toReal : NNReal → ℝ

Coercion ℝ≥0 → ℝ.

@[instance_reducible]

instance NNReal.instCoeReal : Coe NNReal ℝ

def NNReal.mk (x : ℝ) (hx : 0 ≤ x) : NNReal

Constructor of ℝ≥0 from a nonnegative real number.

Important: You should use NNReal.mk instead of the anonymous constructor ⟨_, _⟩ to avoid abuse of the definitional equality between ℝ≥0 and { r : ℝ // 0 ≤ r }.

@[instance_reducible]

instance NNReal.instZero : Zero NNReal

@[instance_reducible]

instance NNReal.instOne : One NNReal

@[instance_reducible]

instance NNReal.instBot : Bot NNReal

@[instance_reducible]

instance NNReal.instOrderBot : OrderBot NNReal

@[instance_reducible]

instance NNReal.instAddCancelCommMonoid : AddCancelCommMonoid NNReal

@[instance_reducible]

instance NNReal.instDistribLattice : DistribLattice NNReal

instance NNReal.instIsOrderedRing : IsOrderedRing NNReal

instance NNReal.instNontrivial : Nontrivial NNReal

instance NNReal.instArchimedean : Archimedean NNReal

@[instance_reducible]

instance NNReal.instSemiring : Semiring NNReal

instance NNReal.instOrderedSub : OrderedSub NNReal

instance NNReal.instIsStrictOrderedRing : IsStrictOrderedRing NNReal

@[instance_reducible]

instance NNReal.instCommSemiring : CommSemiring NNReal

instance NNReal.instCanonicallyOrderedAdd : CanonicallyOrderedAdd NNReal

@[instance_reducible]

instance NNReal.instPartialOrder : PartialOrder NNReal

@[instance_reducible]

instance NNReal.instInhabited : Inhabited NNReal

@[instance_reducible]

instance NNReal.instCommMonoidWithZero : CommMonoidWithZero NNReal

@[instance_reducible]

instance NNReal.instSemilatticeSup : SemilatticeSup NNReal

@[instance_reducible]

instance NNReal.instSemilatticeInf : SemilatticeInf NNReal

@[instance_reducible]

instance NNReal.instSub : Sub NNReal

instance NNReal.instDenselyOrdered : DenselyOrdered NNReal

instance NNReal.instMulArchimedean : MulArchimedean NNReal

instance NNReal.instNoZeroDivisors : NoZeroDivisors NNReal

@[instance_reducible]

noncomputable instance NNReal.instLinearOrder : LinearOrder NNReal

@[instance_reducible]

instance NNReal.instNNRatCast : NNRatCast NNReal

@[instance_reducible]

noncomputable instance NNReal.instInv : Inv NNReal

@[instance_reducible]

noncomputable instance NNReal.instDiv : Div NNReal

@[instance_reducible]

noncomputable instance NNReal.instSMulNNRat : SMul ℚ≥0 NNReal

@[instance_reducible]

noncomputable instance NNReal.zpow : Pow NNReal ℤ

@[instance_reducible]

noncomputable instance NNReal.instSemifield : Semifield NNReal

Redo the Nonneg.semifield instance, because this will get unfolded a lot, and ends up inserting the non-reducible defeq ℝ≥0 = { x // x ≥ 0 } in places where it needs to be reducible(-with-instances).

instance NNReal.instIsOrderedRing_1 : IsOrderedRing NNReal

instance NNReal.instIsStrictOrderedRing_1 : IsStrictOrderedRing NNReal

@[instance_reducible]

noncomputable instance NNReal.instLinearOrderedCommGroupWithZero : LinearOrderedCommGroupWithZero NNReal

@[simp]

theorem NNReal.mk_coe (a : NNReal) (ha : 0 ≤ ↑a) : NNReal.mk (↑a) ha = a

@[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 (NNReal.mk x hx)

theorem NNReal.exists {p : NNReal → Prop} : (∃ (x : NNReal), p x) ↔ ∃ (x : ℝ) (hx : 0 ≤ x), p (NNReal.mk x hx)

def Real.toNNReal (r : ℝ) : NNReal

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

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

theorem Real.toNNReal_of_nonneg {r : ℝ} (hr : 0 ≤ r) : r.toNNReal = NNReal.mk r hr

theorem Real.le_coe_toNNReal (r : ℝ) : r ≤ ↑r.toNNReal

theorem NNReal.coe_nonneg (r : NNReal) : 0 ≤ ↑r

@[simp]

theorem NNReal.not_toReal_neg {r : NNReal} : ¬↑r < 0

@[simp]

theorem NNReal.coe_mk (a : ℝ) (ha : 0 ≤ a) : ↑(NNReal.mk 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 : NNReal.mk 0 ⋯ = 0

@[simp]

theorem NNReal.mk_one : NNReal.mk 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?

@[simp]

theorem NNReal.coe_toRealHom : ⇑toRealHom = toReal

@[instance_reducible]

instance NNReal.instSMulOfReal {M : Type u_1} [SMul ℝ M] : SMul NNReal M

A scalar multiplication over ℝ restricts to a scalar multiplication over ℝ≥0.

@[instance_reducible]

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

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

theorem NNReal.smul_def {M : Type u_1} [SMul ℝ 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_reducible]

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

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

@[instance_reducible]

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

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

@[instance_reducible]

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

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

@[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 Real.toNNReal_monotone : Monotone toNNReal

theorem Real.toNNReal_mono {r₁ r₂ : ℝ} (h : r₁ ≤ r₂) : r₁.toNNReal ≤ r₂.toNNReal

@[simp]

theorem Real.toNNReal_coe {r : NNReal} : (↑r).toNNReal = r

@[simp]

theorem NNReal.mk_natCast (n : ℕ) : NNReal.mk ↑n ⋯ = ↑n

@[simp]

theorem Real.toNNReal_natCast (n : ℕ) : (↑n).toNNReal = ↑n

@[deprecated Real.toNNReal_natCast (since := "2026-05-19")]

theorem Real.toNNReal_coe_nat (n : ℕ) : (↑n).toNNReal = ↑n

Alias of Real.toNNReal_natCast.

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

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.

@[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), NNReal.mk 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)

@[instance_reducible]

noncomputable instance NNReal.instConditionallyCompleteLinearOrderBot : ConditionallyCompleteLinearOrderBot NNReal

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 : sInf ∅ = 0

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 : ⊥ = 0

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.instIsStrictOrderedModule {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [Module ℝ M] [IsStrictOrderedModule ℝ M] : IsStrictOrderedModule NNReal M

@[simp]

theorem Real.coe_toNNReal' (r : ℝ) : ↑r.toNNReal = max r 0

@[simp]

theorem Real.toNNReal_zero : toNNReal 0 = 0

@[simp]

theorem Real.toNNReal_one : toNNReal 1 = 1

@[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_mk {r : ℝ} (hr : 0 ≤ r) : (NNReal.mk r hr)⁻¹ = NNReal.mk r⁻¹ ⋯

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

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.

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

@[simp]

theorem Real.nnabs_natCast (n : ℕ) : nnabs ↑n = ↑n

@[simp]

theorem Real.nnabs_ofNat (n : ℕ) [n.AtLeastTwo] : nnabs (OfNat.ofNat n) = OfNat.ofNat n

theorem Real.cast_natAbs_eq_nnabs_cast (n : ℤ) : ↑n.natAbs = nnabs ↑n

@[simp]

theorem Real.nnabs_pos {x : ℝ} : 0 < nnabs x ↔ x ≠ 0

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.

@[instance_reducible]

unsafe instance instReprNNReal : Repr NNReal

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

theorem Mathlib.Meta.Positivity.nnreal_coe_pos {r : NNReal} : 0 < r → 0 < ↑r

Alias of the reverse direction of NNReal.coe_pos.

def Mathlib.Meta.Positivity.evalNNRealtoReal : PositivityExt

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

def Mathlib.Meta.Positivity.evalRealToNNReal : PositivityExt

Extension for the positivity tactic: Real.toNNReal

theorem Mathlib.Meta.Positivity.nnabs_pos_of_pos {x : ℝ} : x ≠ 0 → 0 < Real.nnabs x

Alias of the reverse direction of Real.nnabs_pos.

def Mathlib.Meta.Positivity.evalRealNNAbs : PositivityExt

Extension for the positivity tactic: Real.nnabs

def NNReal.recToNNReal {C : NNReal → Sort u_1} (mk : (x : ℝ) → 0 ≤ x → C x.toNNReal) (t : NNReal) : C t

A Subtype.mk-free eliminator for ℝ≥0, exposing the underlying real and its nonnegativity. Used by the basify tactic: a goal mentioning ⟨x, hx⟩ : ℝ≥0 is not type-correct at the transparency simp checks at, because ℝ≥0 is semireducible.