Documentation

Mathlib.Data.NNReal.Basic

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;
- CanonicallyOrderedCommSemiring ℝ≥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.OrderedRing.
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.

Equations

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

def NNReal.«termℝ≥0» :

Lean.ParserDescr

Equations

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

noncomputable instance NNReal.instFloorSemiring :

FloorSemiring NNReal

Equations

NNReal.instFloorSemiring = Nonneg.floorSemiring

instance NNReal.instDenselyOrdered :

DenselyOrdered NNReal

Equations

NNReal.instDenselyOrdered = ⋯

instance NNReal.instOrderBot :

OrderBot NNReal

Equations

NNReal.instOrderBot = inferInstance

instance NNReal.instArchimedean :

Archimedean NNReal

Equations

NNReal.instArchimedean = ⋯

instance NNReal.instMulArchimedean :

MulArchimedean NNReal

Equations

NNReal.instMulArchimedean = ⋯

noncomputable instance NNReal.instSub :

Equations

NNReal.instSub = Nonneg.sub

noncomputable instance NNReal.instOrderedSub :

OrderedSub NNReal

Equations

NNReal.instOrderedSub = ⋯

noncomputable instance NNReal.instCanonicallyLinearOrderedSemifield :

CanonicallyLinearOrderedSemifield NNReal

Equations

NNReal.instCanonicallyLinearOrderedSemifield = Nonneg.canonicallyLinearOrderedSemifield

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 NNReal.toReal fun (r : ℝ) => 0 ≤ r

Equations

NNReal.canLift = ⋯

theorem NNReal.eq_iff {n : NNReal} {m : NNReal} :

n = m ↔ ↑n = ↑m

theorem NNReal.eq {n : NNReal} {m : NNReal} :

↑n = ↑m → n = m

theorem NNReal.ne_iff {x : NNReal} {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⟩

noncomputable 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 NNReal.toReal

@[simp]

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

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

@[deprecated NNReal.coe_inj]

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

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

Alias of NNReal.coe_inj.

@[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₁ : NNReal) (r₂ : NNReal) :

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

@[simp]

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

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

@[simp]

theorem NNReal.coe_inv (r : NNReal) :

↑r⁻¹ = (↑r)⁻¹

@[simp]

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

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

theorem NNReal.coe_two :

↑2 = 2

@[simp]

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

Porting note (#11215): 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 :

⇑NNReal.toRealHom = NNReal.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

Equations

⋯ = ⋯

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

SMulCommClass NNReal M N

Equations

⋯ = ⋯

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

SMulCommClass M NNReal N

Equations

⋯ = ⋯

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 = Algebra.mk ((algebraMap ℝ A).comp NNReal.toRealHom) ⋯ ⋯

@[simp]

theorem NNReal.coe_indicator {α : Type u_1} (s : Set α) (f : α → NNReal) (a : α) :

↑(s.indicator f a) = s.indicator (fun (x : α) => ↑(f x)) a

@[simp]

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

↑(r ^ n) = ↑r ^ n

@[simp]

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

↑(r ^ n) = ↑r ^ n

theorem NNReal.coe_list_sum (l : List NNReal) :

↑l.sum = (List.map NNReal.toReal l).sum

theorem NNReal.coe_list_prod (l : List NNReal) :

↑l.prod = (List.map NNReal.toReal l).prod

theorem NNReal.coe_multiset_sum (s : Multiset NNReal) :

↑s.sum = (Multiset.map NNReal.toReal s).sum

theorem NNReal.coe_multiset_prod (s : Multiset NNReal) :

↑s.prod = (Multiset.map NNReal.toReal s).prod

@[simp]

theorem NNReal.coe_sum {ι : Type u_1} (s : Finset ι) (f : ι → NNReal) :

↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)

@[simp]

theorem NNReal.coe_expect {ι : Type u_1} (s : Finset ι) (f : ι → NNReal) :

↑(s.expect fun (i : ι) => f i) = s.expect fun (i : ι) => ↑(f i)

theorem Real.toNNReal_sum_of_nonneg {ι : Type u_1} {s : Finset ι} {f : ι → ℝ} (hf : ∀ i ∈ s, 0 ≤ f i) :

(∑ a ∈ s, f a).toNNReal = ∑ a ∈ s, (f a).toNNReal

@[simp]

theorem NNReal.coe_prod {ι : Type u_1} (s : Finset ι) (f : ι → NNReal) :

↑(∏ a ∈ s, f a) = ∏ a ∈ s, ↑(f a)

theorem Real.toNNReal_prod_of_nonneg {ι : Type u_1} {s : Finset ι} {f : ι → ℝ} (hf : ∀ a ∈ s, 0 ≤ f a) :

(∏ a ∈ s, f a).toNNReal = ∏ a ∈ s, (f a).toNNReal

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

@[deprecated NNReal.coe_natCast]

theorem NNReal.coe_nat_cast (n : ℕ) :

↑↑n = ↑n

Alias of NNReal.coe_natCast.

@[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 ℝ) = NNReal.toReal

@[simp]

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

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

@[simp]

theorem NNReal.coe_lt_coe {r₁ : NNReal} {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 NNReal.toReal

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

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

Alias for the use of gcongr

theorem Real.toNNReal_mono :

Monotone Real.toNNReal

@[simp]

theorem Real.toNNReal_coe {r : NNReal} :

(↑r).toNNReal = r

@[simp]

theorem NNReal.mk_natCast (n : ℕ) :

⟨↑n, ⋯⟩ = ↑n

@[deprecated NNReal.mk_natCast]

theorem NNReal.mk_coe_nat (n : ℕ) :

⟨↑n, ⋯⟩ = ↑n

Alias of NNReal.mk_natCast.

@[simp]

theorem NNReal.toNNReal_coe_nat (n : ℕ) :

(↑n).toNNReal = ↑n

@[simp]

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

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

noncomputable def NNReal.gi :

GaloisInsertion Real.toNNReal NNReal.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 α

Equations

⋯ = ⋯

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

SMulPosStrictMono NNReal α

Equations

⋯ = ⋯

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

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

theorem NNReal.bddAbove_coe {s : Set NNReal} :

BddAbove (NNReal.toReal '' s) ↔ BddAbove s

theorem NNReal.bddBelow_coe (s : Set NNReal) :

BddBelow (NNReal.toReal '' s)

noncomputable instance NNReal.instConditionallyCompleteLinearOrderBot :

ConditionallyCompleteLinearOrderBot NNReal

Equations

NNReal.instConditionallyCompleteLinearOrderBot = Nonneg.conditionallyCompleteLinearOrderBot 0

theorem NNReal.coe_sSup (s : Set NNReal) :

↑(sSup s) = sSup (NNReal.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 (NNReal.toReal '' s)

@[simp]

theorem NNReal.sInf_empty :

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

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

theorem NNReal.le_iInf_add_iInf {ι : Sort u_2} {ι' : Sort u_3} [Nonempty ι] [Nonempty ι'] {f : ι → NNReal} {g : ι' → NNReal} {a : NNReal} (h : ∀ (i : ι) (j : ι'), a ≤ f i + g j) :

a ≤ (⨅ (i : ι), f i) + ⨅ (j : ι'), g j

instance NNReal.covariant_add :

CovariantClass NNReal NNReal (fun (x1 x2 : NNReal) => x1 + x2) fun (x1 x2 : NNReal) => x1 ≤ x2

Equations

NNReal.covariant_add = ⋯

instance NNReal.contravariant_add :

ContravariantClass NNReal NNReal (fun (x1 x2 : NNReal) => x1 + x2) fun (x1 x2 : NNReal) => x1 < x2

Equations

NNReal.contravariant_add = ⋯

instance NNReal.covariant_mul :

CovariantClass NNReal NNReal (fun (x1 x2 : NNReal) => x1 * x2) fun (x1 x2 : NNReal) => x1 ≤ x2

Equations

NNReal.covariant_mul = ⋯

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

a ≤ b

theorem NNReal.lt_iff_exists_rat_btwn (a : NNReal) (b : NNReal) :

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

theorem NNReal.bot_eq_zero :

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

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

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

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

theorem NNReal.mul_finset_sup {α : Type u_2} (r : NNReal) (s : Finset α) (f : α → NNReal) :

r * s.sup f = s.sup fun (a : α) => r * f a

theorem NNReal.finset_sup_mul {α : Type u_2} (s : Finset α) (f : α → NNReal) (r : NNReal) :

s.sup f * r = s.sup fun (a : α) => f a * r

theorem NNReal.finset_sup_div {α : Type u_2} {f : α → NNReal} {s : Finset α} (r : NNReal) :

s.sup f / r = s.sup fun (a : α) => f a / r

@[simp]

theorem NNReal.coe_max (x : NNReal) (y : NNReal) :

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

@[simp]

theorem NNReal.coe_min (x : NNReal) (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} [OrderedAddCommMonoid M] [Module ℝ M] [OrderedSMul ℝ M] :

OrderedSMul NNReal M

Equations

⋯ = ⋯

@[simp]

theorem Real.coe_toNNReal' (r : ℝ) :

↑r.toNNReal = max r 0

@[simp]

theorem Real.toNNReal_zero :

Real.toNNReal 0 = 0

@[simp]

theorem Real.toNNReal_one :

Real.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

@[deprecated Real.toNNReal_eq_natCast]

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

r.toNNReal = ↑n ↔ r = ↑n

Alias of Real.toNNReal_eq_natCast.

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

@[deprecated Real.toNNReal_le_natCast]

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

r.toNNReal ≤ ↑n ↔ r ≤ ↑n

Alias of Real.toNNReal_le_natCast.

@[simp]

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

↑n < r.toNNReal ↔ ↑n < r

@[deprecated Real.natCast_lt_toNNReal]

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

↑n < r.toNNReal ↔ ↑n < r

Alias of Real.natCast_lt_toNNReal.

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

@[deprecated Real.natCastle_toNNReal']

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

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

Alias of Real.natCastle_toNNReal'.

@[simp]

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

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

@[deprecated Real.toNNReal_lt_natCast']

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

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

Alias of Real.toNNReal_lt_natCast'.

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

↑n ≤ r.toNNReal ↔ ↑n ≤ r

@[deprecated Real.natCast_le_toNNReal]

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

↑n ≤ r.toNNReal ↔ ↑n ≤ r

Alias of Real.natCast_le_toNNReal.

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

r.toNNReal < ↑n ↔ r < ↑n

@[deprecated Real.toNNReal_lt_natCast]

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

r.toNNReal < ↑n ↔ r < ↑n

Alias of Real.toNNReal_lt_natCast.

@[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_mul {p : ℝ} {q : ℝ} (hp : 0 ≤ p) :

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

theorem NNReal.mul_eq_mul_left {a : NNReal} {b : NNReal} {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 : NNReal} {b : NNReal} (ha : 0 < a) (hb : b < 1) :

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

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

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

theorem NNReal.exists_mem_Ioc_zpow {x : NNReal} {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. See also mul_tsub and tsub_mul.

theorem NNReal.sub_def {r : NNReal} {p : NNReal} :

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

theorem NNReal.coe_sub_def {r : NNReal} {p : NNReal} :

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

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

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

@[simp]

theorem NNReal.inv_le {r : NNReal} {p : NNReal} (h : r ≠ 0) :

r⁻¹ ≤ p ↔ 1 ≤ r * p

theorem NNReal.inv_le_of_le_mul {r : NNReal} {p : NNReal} (h : 1 ≤ r * p) :

@[simp]

theorem NNReal.le_inv_iff_mul_le {r : NNReal} {p : NNReal} (h : p ≠ 0) :

r ≤ p⁻¹ ↔ r * p ≤ 1

@[simp]

theorem NNReal.lt_inv_iff_mul_lt {r : NNReal} {p : NNReal} (h : p ≠ 0) :

r < p⁻¹ ↔ r * p < 1

@[deprecated le_inv_mul_iff₀]

theorem NNReal.mul_le_iff_le_inv {a : NNReal} {b : NNReal} {r : NNReal} (hr : r ≠ 0) :

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

@[deprecated le_div_iff₀]

theorem NNReal.le_div_iff_mul_le {a : NNReal} {b : NNReal} {r : NNReal} (hr : r ≠ 0) :

a ≤ b / r ↔ a * r ≤ b

@[deprecated div_le_iff₀]

theorem NNReal.div_le_iff {a : NNReal} {b : NNReal} {r : NNReal} (hr : r ≠ 0) :

a / r ≤ b ↔ a ≤ b * r

@[deprecated div_le_iff₀']

theorem NNReal.div_le_iff' {a : NNReal} {b : NNReal} {r : NNReal} (hr : r ≠ 0) :

a / r ≤ b ↔ a ≤ r * b

theorem NNReal.div_le_of_le_mul {a : NNReal} {b : NNReal} {c : NNReal} (h : a ≤ b * c) :

a / c ≤ b

theorem NNReal.div_le_of_le_mul' {a : NNReal} {b : NNReal} {c : NNReal} (h : a ≤ b * c) :

a / b ≤ c

@[deprecated le_div_iff₀]

theorem NNReal.le_div_iff {a : NNReal} {b : NNReal} {r : NNReal} (hr : r ≠ 0) :

a ≤ b / r ↔ a * r ≤ b

@[deprecated le_div_iff₀']

theorem NNReal.le_div_iff' {a : NNReal} {b : NNReal} {r : NNReal} (hr : r ≠ 0) :

a ≤ b / r ↔ r * a ≤ b

@[deprecated div_lt_iff₀]

theorem NNReal.div_lt_iff {a : NNReal} {b : NNReal} {r : NNReal} (hr : r ≠ 0) :

a / r < b ↔ a < b * r

@[deprecated div_lt_iff₀']

theorem NNReal.div_lt_iff' {a : NNReal} {b : NNReal} {r : NNReal} (hr : r ≠ 0) :

a / r < b ↔ a < r * b

@[deprecated lt_div_iff₀]

theorem NNReal.lt_div_iff {a : NNReal} {b : NNReal} {r : NNReal} (hr : r ≠ 0) :

a < b / r ↔ a * r < b

@[deprecated lt_div_iff₀']

theorem NNReal.lt_div_iff' {a : NNReal} {b : NNReal} {r : NNReal} (hr : r ≠ 0) :

a < b / r ↔ r * a < b

theorem NNReal.mul_lt_of_lt_div {a : NNReal} {b : NNReal} {r : NNReal} (h : a < b / r) :

a * r < b

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

a / b ≤ a / c

theorem NNReal.div_le_div_left {a : NNReal} {b : NNReal} {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 : NNReal} {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 : NNReal} {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.zpow_pos {x : NNReal} (hx : x ≠ 0) (n : ℤ) :

0 < x ^ n

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

y⁻¹ < x⁻¹

@[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 NNReal.iInf_mul {ι : Sort u_1} (f : ι → NNReal) (a : NNReal) :

iInf f * a = ⨅ (i : ι), f i * a

theorem NNReal.mul_iInf {ι : Sort u_1} (f : ι → NNReal) (a : NNReal) :

a * iInf f = ⨅ (i : ι), a * f i

theorem NNReal.mul_iSup {ι : Sort u_1} (f : ι → NNReal) (a : NNReal) :

a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i

theorem NNReal.iSup_mul {ι : Sort u_1} (f : ι → NNReal) (a : NNReal) :

(⨆ (i : ι), f i) * a = ⨆ (i : ι), f i * a

theorem NNReal.iSup_div {ι : Sort u_1} (f : ι → NNReal) (a : NNReal) :

(⨆ (i : ι), f i) / a = ⨆ (i : ι), f i / a

theorem NNReal.mul_iSup_le {ι : Sort u_1} {a : NNReal} {g : NNReal} {h : ι → NNReal} (H : ∀ (j : ι), g * h j ≤ a) :

g * iSup h ≤ a

theorem NNReal.iSup_mul_le {ι : Sort u_1} {a : NNReal} {g : ι → NNReal} {h : NNReal} (H : ∀ (i : ι), g i * h ≤ a) :

iSup g * h ≤ a

theorem NNReal.iSup_mul_iSup_le {ι : Sort u_1} {a : NNReal} {g : ι → NNReal} {h : ι → NNReal} (H : ∀ (i j : ι), g i * h j ≤ a) :

iSup g * iSup h ≤ a

theorem NNReal.le_mul_iInf {ι : Sort u_1} [Nonempty ι] {a : NNReal} {g : NNReal} {h : ι → NNReal} (H : ∀ (j : ι), a ≤ g * h j) :

a ≤ g * iInf h

theorem NNReal.le_iInf_mul {ι : Sort u_1} [Nonempty ι] {a : NNReal} {g : ι → NNReal} {h : NNReal} (H : ∀ (i : ι), a ≤ g i * h) :

a ≤ iInf g * h

theorem NNReal.le_iInf_mul_iInf {ι : Sort u_1} [Nonempty ι] {a : NNReal} {g : ι → NNReal} {h : ι → NNReal} (H : ∀ (i j : ι), a ≤ g i * h j) :

a ≤ iInf g * iInf h

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_2, map_one' := Real.nnabs.proof_3, map_mul' := Real.nnabs.proof_4 }

@[simp]

theorem Real.coe_nnabs (x : ℝ) :

↑(Real.nnabs x) = |x|

@[simp]

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

Real.nnabs x = x.toNNReal

theorem Real.nnabs_coe (x : NNReal) :

Real.nnabs ↑x = x

theorem Real.coe_toNNReal_le (x : ℝ) :

↑x.toNNReal ≤ |x|

@[simp]

theorem Real.toNNReal_abs (x : ℝ) :

|x|.toNNReal = Real.nnabs x

theorem Real.cast_natAbs_eq_nnabs_cast (n : ℤ) :

↑n.natAbs = Real.nnabs ↑n

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.

def Mathlib.Meta.Positivity.evalNNRealtoReal :

Mathlib.Meta.Positivity.PositivityExt

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