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

• 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 : Type

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.instFloorSemiringNNRealToOrderedSemiringInstNNRealOrderedCommSemiring : FloorSemiring NNReal

Equations

• NNReal.instFloorSemiringNNRealToOrderedSemiringInstNNRealOrderedCommSemiring = Nonneg.floorSemiring

instance NNReal.instDenselyOrderedNNRealToLTToPreorderToPartialOrderInstNNRealStrictOrderedSemiring : DenselyOrdered NNReal

Equations

• NNReal.instDenselyOrderedNNRealToLTToPreorderToPartialOrderInstNNRealStrictOrderedSemiring = (_ : DenselyOrdered { x : ℝ // 0 ≤ x })

instance NNReal.instOrderBotNNRealToLEToPreorderToPartialOrderInstNNRealStrictOrderedSemiring : OrderBot NNReal

Equations

• NNReal.instOrderBotNNRealToLEToPreorderToPartialOrderInstNNRealStrictOrderedSemiring = inferInstance

instance NNReal.instArchimedeanNNRealToOrderedAddCommMonoidToOrderedSemiringInstNNRealOrderedCommSemiring : Archimedean NNReal

Equations

• NNReal.instArchimedeanNNRealToOrderedAddCommMonoidToOrderedSemiringInstNNRealOrderedCommSemiring = (_ : Archimedean { x : ℝ // 0 ≤ x })

noncomputable instance NNReal.instSubNNReal : Sub NNReal

Equations

• NNReal.instSubNNReal = Nonneg.sub

noncomputable instance NNReal.instOrderedSubNNRealToLEToPreorderToPartialOrderInstNNRealStrictOrderedSemiringToAddToDistribToNonUnitalNonAssocSemiringToNonAssocSemiringInstNNRealSemiringInstSubNNReal : OrderedSub NNReal

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance NNReal.instCanonicallyLinearOrderedSemifieldNNReal : CanonicallyLinearOrderedSemifield NNReal

Equations

• NNReal.instCanonicallyLinearOrderedSemifieldNNReal = Nonneg.canonicallyLinearOrderedSemifield

def NNReal.toReal : NNReal → ℝ

Coercion ℝ≥0 → ℝ.

Equations

• NNReal.toReal = Subtype.val

instance NNReal.instCoeNNRealReal : Coe NNReal ℝ

Equations

• NNReal.instCoeNNRealReal = { 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 = (_ : CanLift ℝ { x : ℝ // 0 ≤ x } Subtype.val fun (r : ℝ) => 0 ≤ r)

theorem NNReal.eq {n : NNReal} {m : NNReal} : ↑n = ↑m → n = m

theorem NNReal.eq_iff {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 { val := x, property := hx }

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

noncomputable def Real.toNNReal (r : ℝ) : NNReal

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

Equations

• Real.toNNReal r = { val := max r 0, property := (_ : 0 ≤ max r 0) }

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

theorem Real.toNNReal_of_nonneg {r : ℝ} (hr : 0 ≤ r) : Real.toNNReal r = { val := r, property := hr }

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

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

@[simp]

theorem NNReal.coe_mk (a : ℝ) (ha : 0 ≤ a) : ↑{ val := a, property := ha } = a

theorem NNReal.coe_injective : Function.Injective NNReal.toReal

@[simp]

theorem NNReal.coe_eq {r₁ : NNReal} {r₂ : NNReal} : ↑r₁ = ↑r₂ ↔ r₁ = r₂

@[simp]

theorem NNReal.coe_zero : ↑0 = 0

@[simp]

theorem NNReal.coe_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

def NNReal.toRealHom : NNReal →+* ℝ

Coercion ℝ≥0 → ℝ as a RingHom.

Porting note: todo: what if we define Coe ℝ≥0 ℝ using this function?

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NNReal.coe_toRealHom : ⇑NNReal.toRealHom = NNReal.toReal

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

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

Equations

• NNReal.instMulActionNNRealToMonoidToMonoidWithZeroInstNNRealSemiring = 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.instIsScalarTowerNNRealToSMulToMonoidToMonoidWithZeroInstNNRealSemiringInstMulActionNNRealToMonoidToMonoidWithZeroInstNNRealSemiringToSMulInstMulActionNNRealToMonoidToMonoidWithZeroInstNNRealSemiring {M : Type u_1} {N : Type u_2} [MulAction ℝ M] [MulAction ℝ N] [SMul M N] [IsScalarTower ℝ M N] : IsScalarTower NNReal M N

Equations

• (_ : IsScalarTower NNReal 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

Equations

• (_ : SMulCommClass NNReal 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

Equations

• (_ : SMulCommClass M NNReal N) = (_ : SMulCommClass M NNReal N)

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

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

Equations

• NNReal.instDistribMulActionNNRealToMonoidToMonoidWithZeroInstNNRealSemiring = DistribMulAction.compHom M ↑NNReal.toRealHom

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

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

Equations

• NNReal.instModuleNNRealInstNNRealSemiring = Module.compHom M NNReal.toRealHom

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

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

Equations

• One or more equations did not get rendered due to their size.

instance NNReal.instStarRingNNRealToNonUnitalNonAssocSemiringToNonAssocSemiringInstNNRealSemiring : StarRing NNReal

Equations

• One or more equations did not get rendered due to their size.

instance NNReal.instTrivialStarNNRealToStarToInvolutiveStarToAddMonoidToAddMonoidWithOneToAddCommMonoidWithOneToNonAssocSemiringInstNNRealSemiringToStarAddMonoidToNonUnitalNonAssocSemiringInstStarRingNNRealToNonUnitalNonAssocSemiringToNonAssocSemiringInstNNRealSemiring : TrivialStar NNReal

Equations

• One or more equations did not get rendered due to their size.

instance NNReal.instStarModuleNNRealRealToStarToInvolutiveStarToAddMonoidToAddMonoidWithOneToAddCommMonoidWithOneToNonAssocSemiringInstNNRealSemiringToStarAddMonoidToNonUnitalNonAssocSemiringInstStarRingNNRealToNonUnitalNonAssocSemiringToNonAssocSemiringInstNNRealSemiringInstAddMonoidRealToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingCommRingInstStarRingRealToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingCommRingToSMulInstNNRealCommSemiringSemiringInstAlgebraNNRealInstNNRealCommSemiringIdInstCommSemiringReal : StarModule NNReal ℝ

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NNReal.coe_indicator {α : Type u_1} (s : Set α) (f : α → NNReal) (a : α) : ↑(Set.indicator s f a) = Set.indicator s (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) : ↑(List.sum l) = List.sum (List.map NNReal.toReal l)

theorem NNReal.coe_list_prod (l : List NNReal) : ↑(List.prod l) = List.prod (List.map NNReal.toReal l)

theorem NNReal.coe_multiset_sum (s : Multiset NNReal) : ↑(Multiset.sum s) = Multiset.sum (Multiset.map NNReal.toReal s)

theorem NNReal.coe_multiset_prod (s : Multiset NNReal) : ↑(Multiset.prod s) = Multiset.prod (Multiset.map NNReal.toReal s)

theorem NNReal.coe_sum {α : Type u_1} {s : Finset α} {f : α → NNReal} : ↑(Finset.sum s fun (a : α) => f a) = Finset.sum s fun (a : α) => ↑(f a)

theorem Real.toNNReal_sum_of_nonneg {α : Type u_1} {s : Finset α} {f : α → ℝ} (hf : ∀ a ∈ s, 0 ≤ f a) : Real.toNNReal (Finset.sum s fun (a : α) => f a) = Finset.sum s fun (a : α) => Real.toNNReal (f a)

theorem NNReal.coe_prod {α : Type u_1} {s : Finset α} {f : α → NNReal} : ↑(Finset.prod s fun (a : α) => f a) = Finset.prod s fun (a : α) => ↑(f a)

theorem Real.toNNReal_prod_of_nonneg {α : Type u_1} {s : Finset α} {f : α → ℝ} (hf : ∀ a ∈ s, 0 ≤ f a) : Real.toNNReal (Finset.prod s fun (a : α) => f a) = Finset.prod s fun (a : α) => Real.toNNReal (f a)

theorem NNReal.coe_nsmul (r : NNReal) (n : ℕ) : ↑(n • r) = n • ↑r

@[simp]

theorem NNReal.coe_nat_cast (n : ℕ) : ↑↑n = ↑n

@[simp]

theorem NNReal.coe_ofNat (n : ℕ) [Nat.AtLeastTwo n] : ↑(OfNat.ofNat n) = OfNat.ofNat n

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

theorem NNReal.coe_mono : Monotone NNReal.toReal

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

theorem Real.toNNReal_mono : Monotone Real.toNNReal

@[simp]

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

@[simp]

theorem NNReal.mk_coe_nat (n : ℕ) : { val := ↑n, property := (_ : 0 ≤ ↑n) } = ↑n

@[simp]

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

@[simp]

theorem Real.toNNReal_ofNat (n : ℕ) [Nat.AtLeastTwo n] : Real.toNNReal (OfNat.ofNat n) = 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 (_ : ∀ (x : NNReal), Real.toNNReal ↑x = x)

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

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

theorem NNReal.orderIsoIccZeroCoe_symm_apply_coe (a : NNReal) (b : ↑(Set.Iic a)) : ↑((OrderIso.symm (NNReal.orderIsoIccZeroCoe a)) b) = ↑↑b

theorem NNReal.coe_image {s : Set NNReal} : NNReal.toReal '' s = {x : ℝ | ∃ (h : 0 ≤ x), { val := x, property := 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.instConditionallyCompleteLinearOrderBotNNReal : ConditionallyCompleteLinearOrderBot NNReal

Equations

• NNReal.instConditionallyCompleteLinearOrderBotNNReal = Nonneg.conditionallyCompleteLinearOrderBot 0

theorem NNReal.coe_sSup (s : Set NNReal) : ↑(sSup s) = sSup (NNReal.toReal '' s)

@[simp]

theorem NNReal.coe_iSup {ι : Sort u_1} (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 : sInf ∅ = 0

theorem NNReal.coe_iInf {ι : Sort u_1} (s : ι → NNReal) : ↑(⨅ (i : ι), s i) = ⨅ (i : ι), ↑(s i)

theorem NNReal.le_iInf_add_iInf {ι : 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

instance NNReal.covariant_add : CovariantClass NNReal NNReal (fun (x x_1 : NNReal) => x + x_1) fun (x x_1 : NNReal) => x ≤ x_1

Equations

• NNReal.covariant_add = (_ : CovariantClass NNReal NNReal (fun (x x_1 : NNReal) => x + x_1) fun (x x_1 : NNReal) => x ≤ x_1)

instance NNReal.contravariant_add : ContravariantClass NNReal NNReal (fun (x x_1 : NNReal) => x + x_1) fun (x x_1 : NNReal) => x < x_1

Equations

• NNReal.contravariant_add = (_ : ContravariantClass NNReal NNReal (fun (x x_1 : NNReal) => x + x_1) fun (x x_1 : NNReal) => x < x_1)

instance NNReal.covariant_mul : CovariantClass NNReal NNReal (fun (x x_1 : NNReal) => x * x_1) fun (x x_1 : NNReal) => x ≤ x_1

Equations

• NNReal.covariant_mul = (_ : CovariantClass NNReal NNReal (fun (x x_1 : NNReal) => x * x_1) fun (x x_1 : NNReal) => x ≤ x_1)

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 < Real.toNNReal ↑q ∧ Real.toNNReal ↑q < b

theorem NNReal.bot_eq_zero : ⊥ = 0

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_1} (r : NNReal) (s : Finset α) (f : α → NNReal) : r * Finset.sup s f = Finset.sup s fun (a : α) => r * f a

theorem NNReal.finset_sup_mul {α : Type u_1} (s : Finset α) (f : α → NNReal) (r : NNReal) : Finset.sup s f * r = Finset.sup s fun (a : α) => f a * r

theorem NNReal.finset_sup_div {α : Type u_1} {f : α → NNReal} {s : Finset α} (r : NNReal) : Finset.sup s f / r = Finset.sup s 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

@[simp]

theorem Real.coe_toNNReal' (r : ℝ) : ↑(Real.toNNReal r) = 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 < Real.toNNReal r ↔ 0 < r

@[simp]

theorem Real.toNNReal_eq_zero {r : ℝ} : Real.toNNReal r = 0 ↔ r ≤ 0

theorem Real.toNNReal_of_nonpos {r : ℝ} : r ≤ 0 → Real.toNNReal r = 0

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

@[simp]

theorem Real.toNNReal_eq_one {r : ℝ} : Real.toNNReal r = 1 ↔ r = 1

@[simp]

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

@[simp]

theorem Real.toNNReal_eq_ofNat {r : ℝ} {n : ℕ} [h : Nat.AtLeastTwo n] : Real.toNNReal r = OfNat.ofNat n ↔ r = OfNat.ofNat n

@[simp]

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

@[simp]

theorem Real.toNNReal_le_one {r : ℝ} : Real.toNNReal r ≤ 1 ↔ r ≤ 1

@[simp]

theorem Real.one_lt_toNNReal {r : ℝ} : 1 < Real.toNNReal r ↔ 1 < r

@[simp]

theorem Real.toNNReal_le_nat_cast {r : ℝ} {n : ℕ} : Real.toNNReal r ≤ ↑n ↔ r ≤ ↑n

@[simp]

theorem Real.nat_cast_lt_toNNReal {r : ℝ} {n : ℕ} : ↑n < Real.toNNReal r ↔ ↑n < r

@[simp]

theorem Real.toNNReal_le_ofNat {r : ℝ} {n : ℕ} [Nat.AtLeastTwo n] : Real.toNNReal r ≤ OfNat.ofNat n ↔ r ≤ ↑n

@[simp]

theorem Real.ofNat_lt_toNNReal {r : ℝ} {n : ℕ} [Nat.AtLeastTwo n] : OfNat.ofNat n < Real.toNNReal r ↔ ↑n < r

@[simp]

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

@[simp]

theorem Real.toNNReal_lt_toNNReal_iff' {r : ℝ} {p : ℝ} : Real.toNNReal r < Real.toNNReal p ↔ r < p ∧ 0 < p

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

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

theorem Real.toNNReal_le_toNNReal_iff' {r : ℝ} {p : ℝ} : Real.toNNReal r ≤ Real.toNNReal p ↔ r ≤ p ∨ r ≤ 0

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

@[simp]

theorem Real.one_le_toNNReal {r : ℝ} : 1 ≤ Real.toNNReal r ↔ 1 ≤ r

@[simp]

theorem Real.toNNReal_lt_one {r : ℝ} : Real.toNNReal r < 1 ↔ r < 1

@[simp]

theorem Real.nat_cast_le_toNNReal' {n : ℕ} {r : ℝ} : ↑n ≤ Real.toNNReal r ↔ ↑n ≤ r ∨ n = 0

@[simp]

theorem Real.toNNReal_lt_nat_cast' {n : ℕ} {r : ℝ} : Real.toNNReal r < ↑n ↔ r < ↑n ∧ n ≠ 0

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

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

@[simp]

theorem Real.toNNReal_lt_ofNat {r : ℝ} {n : ℕ} [h : Nat.AtLeastTwo n] : Real.toNNReal r < OfNat.ofNat n ↔ r < OfNat.ofNat n

@[simp]

theorem Real.ofNat_le_toNNReal {n : ℕ} {r : ℝ} [h : Nat.AtLeastTwo n] : OfNat.ofNat n ≤ Real.toNNReal r ↔ OfNat.ofNat n ≤ r

@[simp]

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

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

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

theorem Real.toNNReal_add_le {r : ℝ} {p : ℝ} : Real.toNNReal (r + p) ≤ Real.toNNReal r + Real.toNNReal p

theorem Real.toNNReal_le_iff_le_coe {r : ℝ} {p : NNReal} : Real.toNNReal r ≤ p ↔ r ≤ ↑p

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

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

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

theorem Real.lt_toNNReal_iff_coe_lt {r : NNReal} {p : ℝ} : r < Real.toNNReal p ↔ ↑r < p

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

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

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 = Real.toNNReal (↑r - ↑p)

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

theorem NNReal.mul_le_iff_le_inv {a : NNReal} {b : NNReal} {r : NNReal} (hr : r ≠ 0) : r * a ≤ b ↔ a ≤ r⁻¹ * b

theorem NNReal.le_div_iff_mul_le {a : NNReal} {b : NNReal} {r : NNReal} (hr : r ≠ 0) : a ≤ b / r ↔ a * r ≤ b

theorem NNReal.div_le_iff {a : NNReal} {b : NNReal} {r : NNReal} (hr : r ≠ 0) : a / r ≤ b ↔ a ≤ b * r

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

theorem NNReal.le_div_iff {a : NNReal} {b : NNReal} {r : NNReal} (hr : r ≠ 0) : a ≤ b / r ↔ a * r ≤ b

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

theorem NNReal.div_lt_iff {a : NNReal} {b : NNReal} {r : NNReal} (hr : r ≠ 0) : a / r < b ↔ a < b * r

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

theorem NNReal.lt_div_iff {a : NNReal} {b : NNReal} {r : NNReal} (hr : r ≠ 0) : a < b / r ↔ a * r < b

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 : ℝ} : Real.toNNReal x⁻¹ = (Real.toNNReal x)⁻¹

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

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

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 ≤ Real.toNNReal y

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.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 : Set.OrdConnected s) : Set.OrdConnected (NNReal.toReal ⁻¹' s)

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

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

theorem Set.OrdConnected.preimage_real_toNNReal {t : Set NNReal} (h : Set.OrdConnected t) : Set.OrdConnected (Real.toNNReal ⁻¹' t)

def Real.nnabs : ℝ →*₀ NNReal

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Real.coe_nnabs (x : ℝ) : ↑(Real.nnabs x) = |x|

@[simp]

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

theorem Real.nnabs_coe (x : NNReal) : Real.nnabs ↑x = x

theorem Real.coe_toNNReal_le (x : ℝ) : ↑(Real.toNNReal x) ≤ |x|

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

def Mathlib.Meta.Positivity.evalNNRealtoReal : Mathlib.Meta.Positivity.PositivityExt

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

Equations

• One or more equations did not get rendered due to their size.