Mathlib.Data.NNReal.Defs

NNReal definition

Full source

/-- Nonnegative real numbers, denoted as `ℝ≥0` withinin the NNReal namespace -/
def NNReal := { r : ℝ // 0 ≤ r } deriving
  Zero, One, Semiring, CommMonoidWithZero, CommSemiring,
  PartialOrder, SemilatticeInf, SemilatticeSup, DistribLattice,
  Nontrivial, Inhabited

Non-negative real numbers

Informal description

The type `ℝ≥0` (also denoted as `NNReal`) represents the non-negative real numbers, defined as the subset of real numbers $r$ such that $0 \leq r$.

NNReal.termℝ≥0 definition

: Lean.ParserDescr✝

Full source

@[inherit_doc] scoped notation "ℝ≥0" => NNReal

Notation for non-negative real numbers

Informal description

The notation `ℝ≥0` is defined as a shorthand for the type `NNReal` of non-negative real numbers.

NNReal.instCanonicallyOrderedAdd instance

: CanonicallyOrderedAdd ℝ≥0

Full source

instance : CanonicallyOrderedAdd ℝ≥0 := Nonneg.canonicallyOrderedAdd

Canonical Ordering of Non-negative Real Numbers

Informal description

The non-negative real numbers $\mathbb{R}_{\geq 0}$ form a canonically ordered additive monoid. That is, for any two non-negative real numbers $a$ and $b$, the inequality $a \leq b$ holds if and only if there exists a non-negative real number $c$ such that $b = a + c$.

NNReal.instNoZeroDivisors instance

: NoZeroDivisors ℝ≥0

Full source

instance : NoZeroDivisors ℝ≥0 := Nonneg.noZeroDivisors

Non-negative Real Numbers Have No Zero Divisors

Informal description

The non-negative real numbers $\mathbb{R}_{\geq 0}$ have no zero divisors. That is, for any $x, y \in \mathbb{R}_{\geq 0}$, if $x \cdot y = 0$, then either $x = 0$ or $y = 0$.

NNReal.instDenselyOrdered instance

: DenselyOrdered ℝ≥0

Full source

instance instDenselyOrdered : DenselyOrdered ℝ≥0 := Nonneg.instDenselyOrdered

Dense Order on Non-negative Real Numbers

Informal description

The non-negative real numbers $\mathbb{R}_{\geq 0}$ are densely ordered. That is, for any two elements $x, y \in \mathbb{R}_{\geq 0}$ with $x < y$, there exists an element $z \in \mathbb{R}_{\geq 0}$ such that $x < z < y$.

NNReal.instOrderBot instance

: OrderBot ℝ≥0

Full source

instance : OrderBot ℝ≥0 := inferInstance

Non-negative Real Numbers as an Ordered Set with Bottom Element

Informal description

The non-negative real numbers $\mathbb{R}_{\geq 0}$ form an ordered set with a bottom element $0$.

NNReal.instArchimedean instance

: Archimedean ℝ≥0

Full source

instance instArchimedean : Archimedean ℝ≥0 := Nonneg.instArchimedean

Archimedean Property of Non-negative Real Numbers

Informal description

The non-negative real numbers $\mathbb{R}_{\geq 0}$ form an Archimedean structure. That is, for any $x, y \in \mathbb{R}_{\geq 0}$ with $0 < y$, there exists a natural number $n$ such that $x \leq n \cdot y$.

NNReal.instMulArchimedean instance

: MulArchimedean ℝ≥0

Full source

instance instMulArchimedean : MulArchimedean ℝ≥0 := Nonneg.instMulArchimedean

Multiplicative Archimedean Property of Non-Negative Real Numbers

Informal description

The non-negative real numbers $\mathbb{R}_{\geq 0}$ form a multiplicatively Archimedean monoid. That is, for any two elements $x, y \in \mathbb{R}_{\geq 0}$ with $1 < y$, there exists a natural number $n$ such that $x \leq y^n$.

NNReal.instMin instance

: Min ℝ≥0

Full source

instance : Min ℝ≥0 := SemilatticeInf.toMin

Minimum Operation on Non-Negative Real Numbers

Informal description

The non-negative real numbers $\mathbb{R}_{\geq 0}$ are equipped with a canonical minimum operation inherited from their meet-semilattice structure.

NNReal.instMax instance

: Max ℝ≥0

Full source

instance : Max ℝ≥0 := SemilatticeSup.toMax

Maximum Operation on Non-Negative Real Numbers

Informal description

The non-negative real numbers $\mathbb{R}_{\geq 0}$ are equipped with a canonical maximum operation, where for any two elements $a, b \in \mathbb{R}_{\geq 0}$, the maximum $\max(a, b)$ is defined as their supremum with respect to the natural order on $\mathbb{R}_{\geq 0}$.

NNReal.instSub instance

: Sub ℝ≥0

Full source

instance : Sub ℝ≥0 := Nonneg.sub

Subtraction Operation on Non-Negative Real Numbers

Informal description

The non-negative real numbers $\mathbb{R}_{\geq 0}$ are equipped with a canonical subtraction operation inherited from the real numbers.

NNReal.instOrderedSub instance

: OrderedSub ℝ≥0

Full source

instance : OrderedSub ℝ≥0 := Nonneg.orderedSub

Ordered Subtraction Structure on Non-Negative Real Numbers

Informal description

The non-negative real numbers $\mathbb{R}_{\geq 0}$ form an ordered subtraction structure, where for any $a, b, c \in \mathbb{R}_{\geq 0}$, the inequality $a - b \leq c$ holds if and only if $a \leq c + b$.

NNReal.instNNRatCast instance

: NNRatCast ℝ≥0

Full source

instance : NNRatCast ℝ≥0 where nnratCast r := ⟨r, r.cast_nonneg⟩

Canonical Homomorphism from Non-Negative Rationals to Non-Negative Reals

Informal description

The non-negative real numbers $\mathbb{R}_{\geq 0}$ are equipped with a canonical homomorphism from the non-negative rational numbers $\mathbb{Q}_{\geq 0}$.

NNReal.instLinearOrder instance

: LinearOrder ℝ≥0

Full source

noncomputable instance : LinearOrder ℝ≥0 :=
  Subtype.instLinearOrder _

Linear Order on Non-Negative Real Numbers

Informal description

The non-negative real numbers $\mathbb{R}_{\geq 0}$ form a linear order with respect to the restriction of the order on $\mathbb{R}$.

NNReal.instSemifield instance

: Semifield ℝ≥0

Full source

noncomputable instance : Semifield ℝ≥0 :=
  Nonneg.semifield

The Semifield Structure on Non-Negative Real Numbers

Informal description

The non-negative real numbers $\mathbb{R}_{\geq 0}$ form a semifield. That is, they are a commutative semiring with multiplicative inverses for all nonzero elements, and the order is compatible with the algebraic operations.

NNReal.instIsOrderedRing instance

: IsOrderedRing ℝ≥0

Full source

instance : IsOrderedRing ℝ≥0 :=
  Nonneg.isOrderedRing

The Ordered Semiring Structure on Non-Negative Real Numbers

Informal description

The non-negative real numbers $\mathbb{R}_{\geq 0}$ form an ordered semiring. That is, they satisfy: 1. Addition is monotone: $a \leq b$ implies $a + c \leq b + c$ for all $c \in \mathbb{R}_{\geq 0}$ 2. Multiplication by nonnegative elements is monotone: if $0 \leq a$ and $b \leq c$ then $a \cdot b \leq a \cdot c$ 3. The inequality $0 \leq 1$ holds

NNReal.instIsStrictOrderedRing instance

: IsStrictOrderedRing ℝ≥0

Full source

instance : IsStrictOrderedRing ℝ≥0 :=
  Nonneg.isStrictOrderedRing

Strict Ordered Ring Structure on Non-Negative Real Numbers

Informal description

The non-negative real numbers $\mathbb{R}_{\geq 0}$ form a strict ordered ring. That is, they satisfy: 1. Addition is strictly monotone: $a < b$ implies $a + c < b + c$ for all $c \in \mathbb{R}_{\geq 0}$ 2. Multiplication by positive elements is strictly monotone: if $0 < a$ and $b < c$ then $a \cdot b < a \cdot c$ 3. The inequality $0 \leq 1$ holds 4. The ring is nontrivial ($0 \neq 1$)

NNReal.instLinearOrderedCommGroupWithZero instance

: LinearOrderedCommGroupWithZero ℝ≥0

Full source

noncomputable instance : LinearOrderedCommGroupWithZero ℝ≥0 :=
  Nonneg.linearOrderedCommGroupWithZero

Non-negative Reals as a Linearly Ordered Commutative Group with Zero

Informal description

The non-negative real numbers $\mathbb{R}_{\geq 0}$ form a linearly ordered commutative group with zero. This means they are equipped with a commutative multiplication operation (with identity 1), a compatible linear order, and every nonzero element has a multiplicative inverse, while also having a zero element that is absorbing for multiplication.

NNReal.toReal definition

: ℝ≥0 → ℝ

Full source

/-- Coercion `ℝ≥0 → ℝ`. -/
@[coe] def toReal : ℝ≥0 → ℝ := Subtype.val

Inclusion of non-negative real numbers into reals

Informal description

The function maps a non-negative real number $ x $ (an element of $\mathbb{R}_{\geq 0}$) to its underlying real number value $ x \in \mathbb{R} $. This is the canonical inclusion map from non-negative reals to all reals.

NNReal.instCoeReal instance

: Coe ℝ≥0 ℝ

Full source

instance : Coe ℝ≥0 ℝ := ⟨toReal⟩

Canonical Embedding of Non-Negative Real Numbers into Reals

Informal description

The non-negative real numbers $\mathbb{R}_{\geq 0}$ can be naturally embedded into the real numbers $\mathbb{R}$ via the canonical inclusion map.

NNReal.val_eq_coe theorem

(n : ℝ≥0) : n.val = n

Full source

@[simp]
theorem val_eq_coe (n : ℝ≥0) : n.val = n :=
  rfl

Equality of Non-Negative Real Number and Its Underlying Value

Informal description

For any non-negative real number $n \in \mathbb{R}_{\geq 0}$, the underlying real value of $n$ is equal to $n$ itself, i.e., $n = n$.

NNReal.canLift instance

: CanLift ℝ ℝ≥0 toReal fun r => 0 ≤ r

Full source

instance canLift : CanLift ℝ ℝ≥0 toReal fun r => 0 ≤ r :=
  Subtype.canLift _

Lifting Non-Negative Real Numbers from Reals

Informal description

There is a canonical way to lift a real number $r$ to a non-negative real number $\mathbb{R}_{\geq 0}$ when $0 \leq r$, using the inclusion map $\mathbb{R}_{\geq 0} \to \mathbb{R}$.

NNReal.eq theorem

{n m : ℝ≥0} : (n : ℝ) = (m : ℝ) → n = m

Full source

@[ext] protected theorem eq {n m : ℝ≥0} : (n : ℝ) = (m : ℝ) → n = m :=
  Subtype.eq

Injective Embedding of Non-Negative Real Numbers into Reals

Informal description

For any two non-negative real numbers $n, m \in \mathbb{R}_{\geq 0}$, if their underlying real values are equal (i.e., $n = m$ as real numbers), then $n = m$ as elements of $\mathbb{R}_{\geq 0}$.

NNReal.ne_iff theorem

{x y : ℝ≥0} : (x : ℝ) ≠ (y : ℝ) ↔ x ≠ y

Full source

theorem ne_iff {x y : ℝ≥0} : (x : ℝ) ≠ (y : ℝ)(x : ℝ) ≠ (y : ℝ) ↔ x ≠ y :=
  not_congr <| NNReal.eq_iff.symm

Inequality Preservation in Non-Negative Reals

Informal description

For any two non-negative real numbers $x, y \in \mathbb{R}_{\geq 0}$, the inequality $x \neq y$ holds in $\mathbb{R}_{\geq 0}$ if and only if their images under the canonical inclusion into $\mathbb{R}$ satisfy $x \neq y$.

NNReal.forall theorem

{p : ℝ≥0 → Prop} : (∀ x : ℝ≥0, p x) ↔ ∀ (x : ℝ) (hx : 0 ≤ x), p ⟨x, hx⟩

Full source

protected theorem «forall» {p : ℝ≥0 → Prop} :
    (∀ x : ℝ≥0, p x) ↔ ∀ (x : ℝ) (hx : 0 ≤ x), p ⟨x, hx⟩ :=
  Subtype.forall

Universal Quantification over Non-Negative Real Numbers via Real Numbers

Informal description

For any predicate $p$ on non-negative real numbers $\mathbb{R}_{\geq 0}$, the universal quantification $\forall x \in \mathbb{R}_{\geq 0}, p(x)$ holds if and only if for every real number $x \in \mathbb{R}$ with $0 \leq x$, the predicate $p$ holds for the canonical embedding of $x$ into $\mathbb{R}_{\geq 0}$ (i.e., $p(\langle x, hx \rangle)$ where $hx$ is the proof that $0 \leq x$).

NNReal.exists theorem

{p : ℝ≥0 → Prop} : (∃ x : ℝ≥0, p x) ↔ ∃ (x : ℝ) (hx : 0 ≤ x), p ⟨x, hx⟩

Full source

protected theorem «exists» {p : ℝ≥0 → Prop} :
    (∃ x : ℝ≥0, p x) ↔ ∃ (x : ℝ) (hx : 0 ≤ x), p ⟨x, hx⟩ :=
  Subtype.exists

Existence in Non-Negative Reals via Existence in Reals

Informal description

For any predicate $p$ on non-negative real numbers $\mathbb{R}_{\geq 0}$, there exists an element $x \in \mathbb{R}_{\geq 0}$ satisfying $p(x)$ if and only if there exists a real number $x \in \mathbb{R}$ with $0 \leq x$ such that $p$ holds for the canonical embedding of $x$ into $\mathbb{R}_{\geq 0}$ (i.e., $p(\langle x, hx \rangle)$ where $hx$ is the proof that $0 \leq x$).

Real.toNNReal definition

(r : ℝ) : ℝ≥0

Full source

/-- Reinterpret a real number `r` as a non-negative real number. Returns `0` if `r < 0`. -/
def _root_.Real.toNNReal (r : ℝ) : ℝ≥0 :=
  ⟨max r 0, le_max_right _ _⟩

Non-negative part of a real number

Informal description

The function maps a real number $r$ to the non-negative real number $\max(r, 0)$. If $r$ is non-negative, the result is $r$ itself; otherwise, the result is $0$.

Real.coe_toNNReal theorem

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

Full source

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

Inclusion of Non-Negative Real Part Preserves Non-Negative Reals

Informal description

For any real number $r$ such that $0 \leq r$, the canonical inclusion of the non-negative part of $r$ (denoted $\text{toNNReal}(r)$) back into the real numbers is equal to $r$ itself, i.e., $\text{toNNReal}(r) = r$.

Real.toNNReal_of_nonneg theorem

{r : ℝ} (hr : 0 ≤ r) : r.toNNReal = ⟨r, hr⟩

Full source

theorem _root_.Real.toNNReal_of_nonneg {r : ℝ} (hr : 0 ≤ r) : r.toNNReal = ⟨r, hr⟩ := by
  simp_rw [Real.toNNReal, max_eq_left hr]

Non-negative part of a non-negative real number equals itself

Informal description

For any real number $r$ such that $0 \leq r$, the non-negative part of $r$ (denoted as $r.\text{toNNReal}$) is equal to the pair $\langle r, hr \rangle$, where $hr$ is the proof that $0 \leq r$.

Real.le_coe_toNNReal theorem

(r : ℝ) : r ≤ Real.toNNReal r

Full source

theorem _root_.Real.le_coe_toNNReal (r : ℝ) : r ≤ Real.toNNReal r :=
  le_max_left r 0

Real number is less than or equal to its non-negative part

Informal description

For any real number $r$, we have $r \leq \text{toNNReal}(r)$, where $\text{toNNReal}(r) = \max(r, 0)$ is the non-negative part of $r$.

NNReal.coe_nonneg theorem

(r : ℝ≥0) : (0 : ℝ) ≤ r

Full source

@[bound] theorem coe_nonneg (r : ℝ≥0) : (0 : ℝ) ≤ r := r.2

Non-negativity of Non-negative Real Numbers

Informal description

For any non-negative real number $r \in \mathbb{R}_{\geq 0}$, the underlying real number satisfies $0 \leq r$.

NNReal.coe_mk theorem

(a : ℝ) (ha) : toReal ⟨a, ha⟩ = a

Full source

@[simp, norm_cast] theorem coe_mk (a : ℝ) (ha) : toReal ⟨a, ha⟩ = a := rfl

Canonical inclusion preserves value for non-negative reals

Informal description

For any real number $a$ and a proof $ha$ that $0 \leq a$, the canonical inclusion map from non-negative real numbers to real numbers satisfies $\text{toReal}(\langle a, ha \rangle) = a$.

NNReal.coe_injective theorem

: Injective ((↑) : ℝ≥0 → ℝ)

Full source

protected theorem coe_injective : Injective ((↑) : ℝ≥0 → ℝ) := Subtype.coe_injective

Injectivity of the Non-negative Real Number Inclusion

Informal description

The canonical inclusion map from non-negative real numbers to real numbers, denoted by $(↑) : \mathbb{R}_{\geq 0} \to \mathbb{R}$, is injective. That is, for any $r_1, r_2 \in \mathbb{R}_{\geq 0}$, if $(↑)r_1 = (↑)r_2$ in $\mathbb{R}$, then $r_1 = r_2$ in $\mathbb{R}_{\geq 0}$.

NNReal.coe_inj theorem

{r₁ r₂ : ℝ≥0} : (r₁ : ℝ) = r₂ ↔ r₁ = r₂

Full source

@[simp, norm_cast] lemma coe_inj {r₁ r₂ : ℝ≥0} : (r₁ : ℝ) = r₂ ↔ r₁ = r₂ :=
  NNReal.coe_injective.eq_iff

Equality of Non-negative Real Numbers via Inclusion into Reals

Informal description

For any two non-negative real numbers $r_1$ and $r_2$ in $\mathbb{R}_{\geq 0}$, the canonical inclusion map into $\mathbb{R}$ satisfies $(r_1 : \mathbb{R}) = r_2$ if and only if $r_1 = r_2$ in $\mathbb{R}_{\geq 0}$.

NNReal.coe_zero theorem

: ((0 : ℝ≥0) : ℝ) = 0

Full source

@[simp, norm_cast] lemma coe_zero : ((0 : ℝ≥0) : ℝ) = 0 := rfl

Inclusion of Zero in Non-negative Reals Preserves Zero

Informal description

The canonical inclusion map from non-negative real numbers to real numbers maps the zero element of $\mathbb{R}_{\geq 0}$ to the zero element of $\mathbb{R}$, i.e., $(0 : \mathbb{R}_{\geq 0}) = 0 \in \mathbb{R}$.

NNReal.coe_one theorem

: ((1 : ℝ≥0) : ℝ) = 1

Full source

@[simp, norm_cast] lemma coe_one : ((1 : ℝ≥0) : ℝ) = 1 := rfl

Inclusion of One in Non-negative Reals Preserves One

Informal description

The canonical inclusion map from non-negative real numbers to real numbers maps the multiplicative identity element of $\mathbb{R}_{\geq 0}$ to the multiplicative identity element of $\mathbb{R}$, i.e., $(1 : \mathbb{R}_{\geq 0}) = 1 \in \mathbb{R}$.

NNReal.mk_zero theorem

: (⟨0, le_rfl⟩ : ℝ≥0) = 0

Full source

@[simp] lemma mk_zero : (⟨0, le_rfl⟩ : ℝ≥0) = 0 := rfl

Zero Construction in Nonnegative Reals

Informal description

The nonnegative real number constructed from the real number $0$ with the proof that $0 \leq 0$ is equal to the zero element of $\mathbb{R}_{\geq 0}$.

NNReal.mk_one theorem

: (⟨1, zero_le_one⟩ : ℝ≥0) = 1

Full source

@[simp] lemma mk_one : (⟨1, zero_le_one⟩ : ℝ≥0) = 1 := rfl

One Construction in Nonnegative Reals

Informal description

The nonnegative real number constructed from the real number $1$ with the proof that $0 \leq 1$ is equal to the multiplicative identity element of $\mathbb{R}_{\geq 0}$.

NNReal.coe_add theorem

(r₁ r₂ : ℝ≥0) : ((r₁ + r₂ : ℝ≥0) : ℝ) = r₁ + r₂

Full source

@[simp, norm_cast]
protected theorem coe_add (r₁ r₂ : ℝ≥0) : ((r₁ + r₂ : ℝ≥0) : ℝ) = r₁ + r₂ :=
  rfl

Inclusion Preserves Addition in Non-Negative Reals

Informal description

For any two non-negative real numbers $r_1$ and $r_2$ in $\mathbb{R}_{\geq 0}$, the canonical inclusion map applied to their sum in $\mathbb{R}_{\geq 0}$ equals the sum of their images in $\mathbb{R}$, i.e., $(r_1 + r_2 : \mathbb{R}_{\geq 0}) = r_1 + r_2$ as real numbers.

NNReal.coe_mul theorem

(r₁ r₂ : ℝ≥0) : ((r₁ * r₂ : ℝ≥0) : ℝ) = r₁ * r₂

Full source

@[simp, norm_cast]
protected theorem coe_mul (r₁ r₂ : ℝ≥0) : ((r₁ * r₂ : ℝ≥0) : ℝ) = r₁ * r₂ :=
  rfl

Multiplication Preservation in Non-Negative Real Numbers Inclusion

Informal description

For any two non-negative real numbers $r_1$ and $r_2$ in $\mathbb{R}_{\geq 0}$, the canonical inclusion map to $\mathbb{R}$ preserves multiplication, i.e., $(r_1 \cdot r_2) = r_1 \cdot r_2$ where the left-hand side multiplication is in $\mathbb{R}_{\geq 0}$ and the right-hand side is in $\mathbb{R}$.

NNReal.coe_inv theorem

(r : ℝ≥0) : ((r⁻¹ : ℝ≥0) : ℝ) = (r : ℝ)⁻¹

Full source

@[simp, norm_cast]
protected theorem coe_inv (r : ℝ≥0) : ((r⁻¹ : ℝ≥0) : ℝ) = (r : ℝ)⁻¹ :=
  rfl

Preservation of Multiplicative Inverse in Non-negative Reals

Informal description

For any non-negative real number $r \in \mathbb{R}_{\geq 0}$, the canonical inclusion map $\mathbb{R}_{\geq 0} \to \mathbb{R}$ preserves the multiplicative inverse, i.e., $(r^{-1}) = (r)^{-1}$.

NNReal.coe_div theorem

(r₁ r₂ : ℝ≥0) : ((r₁ / r₂ : ℝ≥0) : ℝ) = (r₁ : ℝ) / r₂

Full source

@[simp, norm_cast]
protected theorem coe_div (r₁ r₂ : ℝ≥0) : ((r₁ / r₂ : ℝ≥0) : ℝ) = (r₁ : ℝ) / r₂ :=
  rfl

Inclusion Preserves Division of Non-negative Real Numbers

Informal description

For any non-negative real numbers $r_1, r_2 \in \mathbb{R}_{\geq 0}$, the canonical inclusion map into $\mathbb{R}$ satisfies $(r_1 / r_2 : \mathbb{R}) = r_1 / r_2$.

NNReal.coe_two theorem

: ((2 : ℝ≥0) : ℝ) = 2

Full source

protected theorem coe_two : ((2 : ℝ≥0) : ℝ) = 2 := rfl

Inclusion of 2 in Non-negative Reals Preserves Value

Informal description

The canonical inclusion map from non-negative real numbers to real numbers maps the element $2 \in \mathbb{R}_{\geq 0}$ to $2 \in \mathbb{R}$.

NNReal.coe_sub theorem

{r₁ r₂ : ℝ≥0} (h : r₂ ≤ r₁) : ((r₁ - r₂ : ℝ≥0) : ℝ) = ↑r₁ - ↑r₂

Full source

@[simp, norm_cast]
protected theorem coe_sub {r₁ r₂ : ℝ≥0} (h : r₂ ≤ r₁) : ((r₁ - r₂ : ℝ≥0) : ℝ) = ↑r₁ - ↑r₂ :=
  max_eq_left <| le_sub_comm.2 <| by simp [show (r₂ : ℝ) ≤ r₁ from h]

Inclusion Preserves Subtraction of Non-negative Real Numbers

Informal description

For any non-negative real numbers $r_1, r_2 \in \mathbb{R}_{\geq 0}$ such that $r_2 \leq r_1$, the canonical inclusion map into $\mathbb{R}$ satisfies $(r_1 - r_2 : \mathbb{R}) = r_1 - r_2$.

NNReal.coe_eq_zero theorem

: (r : ℝ) = 0 ↔ r = 0

Full source

@[simp, norm_cast] lemma coe_eq_zero : (r : ℝ) = 0 ↔ r = 0 := by rw [← coe_zero, coe_inj]

Inclusion of Non-negative Real Number is Zero if and only if It is Zero

Informal description

For any non-negative real number $r \in \mathbb{R}_{\geq 0}$, the canonical inclusion map into $\mathbb{R}$ satisfies $(r : \mathbb{R}) = 0$ if and only if $r = 0$ in $\mathbb{R}_{\geq 0}$.

NNReal.coe_eq_one theorem

: (r : ℝ) = 1 ↔ r = 1

Full source

@[simp, norm_cast] lemma coe_eq_one : (r : ℝ) = 1 ↔ r = 1 := by rw [← coe_one, coe_inj]

Equivalence of One in Non-negative Reals and Reals

Informal description

For any non-negative real number $r \in \mathbb{R}_{\geq 0}$, the canonical inclusion map into $\mathbb{R}$ satisfies $(r : \mathbb{R}) = 1$ if and only if $r = 1$ in $\mathbb{R}_{\geq 0}$.

NNReal.coe_ne_zero theorem

: (r : ℝ) ≠ 0 ↔ r ≠ 0

Full source

@[norm_cast] lemma coe_ne_zero : (r : ℝ) ≠ 0(r : ℝ) ≠ 0 ↔ r ≠ 0 := coe_eq_zero.not

Non-zero Criterion for Non-negative Real Numbers via Inclusion

Informal description

For any non-negative real number $r \in \mathbb{R}_{\geq 0}$, the canonical inclusion map into $\mathbb{R}$ satisfies $(r : \mathbb{R}) \neq 0$ if and only if $r \neq 0$ in $\mathbb{R}_{\geq 0}$.

NNReal.coe_ne_one theorem

: (r : ℝ) ≠ 1 ↔ r ≠ 1

Full source

@[norm_cast] lemma coe_ne_one : (r : ℝ) ≠ 1(r : ℝ) ≠ 1 ↔ r ≠ 1 := coe_eq_one.not

Non-one Criterion for Non-negative Real Numbers via Inclusion

Informal description

For any non-negative real number $r \in \mathbb{R}_{\geq 0}$, the canonical inclusion map into $\mathbb{R}$ satisfies $(r : \mathbb{R}) \neq 1$ if and only if $r \neq 1$ in $\mathbb{R}_{\geq 0}$.

NNReal.toRealHom definition

: ℝ≥0 →+* ℝ

Full source

/-- Coercion `ℝ≥0 → ℝ` as a `RingHom`.

TODO: what if we define `Coe ℝ≥0 ℝ` using this function? -/
def toRealHom : ℝ≥0ℝ≥0 →+* ℝ where
  toFun := (↑)
  map_one' := NNReal.coe_one
  map_mul' := NNReal.coe_mul
  map_zero' := NNReal.coe_zero
  map_add' := NNReal.coe_add

Inclusion ring homomorphism from non-negative reals to reals

Informal description

The ring homomorphism from the non-negative real numbers $\mathbb{R}_{\geq 0}$ to the real numbers $\mathbb{R}$ is defined by the canonical inclusion map, which preserves the additive and multiplicative structures. Specifically: - It maps $1 \in \mathbb{R}_{\geq 0}$ to $1 \in \mathbb{R}$, - It maps $0 \in \mathbb{R}_{\geq 0}$ to $0 \in \mathbb{R}$, - It preserves addition: $(r_1 + r_2) = r_1 + r_2$ for any $r_1, r_2 \in \mathbb{R}_{\geq 0}$, - It preserves multiplication: $(r_1 \cdot r_2) = r_1 \cdot r_2$ for any $r_1, r_2 \in \mathbb{R}_{\geq 0}$.

NNReal.coe_toRealHom theorem

: ⇑toRealHom = toReal

Full source

@[simp] theorem coe_toRealHom : ⇑toRealHom = toReal := rfl

Ring Homomorphism Inclusion Map Coincides with Canonical Inclusion

Informal description

The underlying function of the ring homomorphism from non-negative real numbers to real numbers is equal to the canonical inclusion map $\mathbb{R}_{\geq 0} \to \mathbb{R}$.

NNReal.instMulActionOfReal instance

{M : Type*} [MulAction ℝ M] : MulAction ℝ≥0 M

Full source

/-- A `MulAction` over `ℝ` restricts to a `MulAction` over `ℝ≥0`. -/
instance {M : Type*} [MulAction ℝ M] : MulAction ℝ≥0 M :=
  MulAction.compHom M toRealHom.toMonoidHom

Multiplicative Action of Non-negative Reals Induced from Reals

Informal description

For any type $M$ with a multiplicative action of the real numbers $\mathbb{R}$, there is an induced multiplicative action of the non-negative real numbers $\mathbb{R}_{\geq 0}$ on $M$, where the action of $r \in \mathbb{R}_{\geq 0}$ on $x \in M$ is given by $r \bullet x = (r : \mathbb{R}) \bullet x$.

NNReal.smul_def theorem

{M : Type*} [MulAction ℝ M] (c : ℝ≥0) (x : M) : c • x = (c : ℝ) • x

Full source

theorem smul_def {M : Type*} [MulAction ℝ M] (c : ℝ≥0) (x : M) : c • x = (c : ℝ) • x :=
  rfl

Scalar Multiplication of Non-negative Reals Coincides with Underlying Reals

Informal description

For any type $M$ with a multiplicative action of the real numbers $\mathbb{R}$, the scalar multiplication of a non-negative real number $c \in \mathbb{R}_{\geq 0}$ on an element $x \in M$ is equal to the scalar multiplication of the underlying real number $c \in \mathbb{R}$ on $x$, i.e., $c \bullet x = (c : \mathbb{R}) \bullet x$.

NNReal.instIsScalarTowerOfReal instance

{M N : Type*} [MulAction ℝ M] [MulAction ℝ N] [SMul M N] [IsScalarTower ℝ M N] : IsScalarTower ℝ≥0 M N

Full source

instance {M N : Type*} [MulAction ℝ M] [MulAction ℝ N] [SMul M N] [IsScalarTower ℝ M N] :
    IsScalarTower ℝ≥0 M N where smul_assoc r := smul_assoc (r : ℝ)

Scalar Tower Property for Non-negative Real Numbers

Informal description

For any types $M$ and $N$ with multiplicative actions of the real numbers $\mathbb{R}$, if there exists a scalar multiplication operation between $M$ and $N$ that forms a scalar tower with $\mathbb{R}$, then the non-negative real numbers $\mathbb{R}_{\geq 0}$ also form a scalar tower with $M$ and $N$. Specifically, for any $r \in \mathbb{R}_{\geq 0}$, $x \in M$, and $y \in N$, the scalar multiplications satisfy $(r \cdot x) \cdot y = r \cdot (x \cdot y)$, where $\cdot$ denotes the respective scalar multiplication operations.

NNReal.smulCommClass_left instance

{M N : Type*} [MulAction ℝ N] [SMul M N] [SMulCommClass ℝ M N] : SMulCommClass ℝ≥0 M N

Full source

instance smulCommClass_left {M N : Type*} [MulAction ℝ N] [SMul M N] [SMulCommClass ℝ M N] :
    SMulCommClass ℝ≥0 M N where smul_comm r := smul_comm (r : ℝ)

Commutativity of Scalar Multiplication with Non-negative Reals

Informal description

For any types $M$ and $N$ with a multiplicative action of the real numbers $\mathbb{R}$ on $N$, and a scalar multiplication operation $M$ on $N$ that commutes with the $\mathbb{R}$-action, the scalar multiplication operation $M$ on $N$ also commutes with the $\mathbb{R}_{\geq 0}$-action. In other words, for any $r \in \mathbb{R}_{\geq 0}$, $m \in M$, and $n \in N$, we have $r \bullet (m \bullet n) = m \bullet (r \bullet n)$.

NNReal.smulCommClass_right instance

{M N : Type*} [MulAction ℝ N] [SMul M N] [SMulCommClass M ℝ N] : SMulCommClass M ℝ≥0 N

Full source

instance smulCommClass_right {M N : Type*} [MulAction ℝ N] [SMul M N] [SMulCommClass M ℝ N] :
    SMulCommClass M ℝ≥0 N where smul_comm m r := smul_comm m (r : ℝ)

Commutativity of Scalar Multiplications by $M$ and Non-negative Reals on $N$

Informal description

For any types $M$ and $N$ with a multiplicative action of $\mathbb{R}$ on $N$, a scalar multiplication operation $M$ on $N$, and a commutativity property between the scalar multiplications by $M$ and $\mathbb{R}$ on $N$, the scalar multiplications by $M$ and $\mathbb{R}_{\geq 0}$ on $N$ also commute. That is, for any $m \in M$, $r \in \mathbb{R}_{\geq 0}$, and $n \in N$, we have $m \cdot (r \cdot n) = r \cdot (m \cdot n)$.

NNReal.instDistribMulActionOfReal instance

{M : Type*} [AddMonoid M] [DistribMulAction ℝ M] : DistribMulAction ℝ≥0 M

Full source

/-- A `DistribMulAction` over `ℝ` restricts to a `DistribMulAction` over `ℝ≥0`. -/
instance {M : Type*} [AddMonoid M] [DistribMulAction ℝ M] : DistribMulAction ℝ≥0 M :=
  DistribMulAction.compHom M toRealHom.toMonoidHom

Distributive Multiplicative Action of Non-negative Reals on Real Modules

Informal description

For any additive monoid $M$ equipped with a distributive multiplicative action by the real numbers $\mathbb{R}$, there is a canonical distributive multiplicative action by the non-negative real numbers $\mathbb{R}_{\geq 0}$ on $M$.

NNReal.instModuleOfReal instance

{M : Type*} [AddCommMonoid M] [Module ℝ M] : Module ℝ≥0 M

Full source

/-- A `Module` over `ℝ` restricts to a `Module` over `ℝ≥0`. -/
instance {M : Type*} [AddCommMonoid M] [Module ℝ M] : Module ℝ≥0 M :=
  Module.compHom M toRealHom

Module Structure on Non-negative Real Numbers

Informal description

For any additive commutative monoid $M$ that is a module over the real numbers $\mathbb{R}$, $M$ is also a module over the non-negative real numbers $\mathbb{R}_{\geq 0}$.

NNReal.instAlgebraOfReal instance

{A : Type*} [Semiring A] [Algebra ℝ A] : Algebra ℝ≥0 A

Full source

/-- An `Algebra` over `ℝ` restricts to an `Algebra` over `ℝ≥0`. -/
instance {A : Type*} [Semiring A] [Algebra ℝ A] : Algebra ℝ≥0 A where
  smul := (· • ·)
  commutes' r x := by simp [Algebra.commutes]
  smul_def' r x := by simp [← Algebra.smul_def (r : ℝ) x, smul_def]
  algebraMap := (algebraMap ℝ A).comp (toRealHom : ℝ≥0 →+* ℝ)

Algebra Structure on Semirings via Non-negative Reals

Informal description

For any semiring $A$ equipped with an algebra structure over the real numbers $\mathbb{R}$, there is a canonical algebra structure over the non-negative real numbers $\mathbb{R}_{\geq 0}$ on $A$.

NNReal.coe_pow theorem

(r : ℝ≥0) (n : ℕ) : ((r ^ n : ℝ≥0) : ℝ) = (r : ℝ) ^ n

Full source

@[simp, norm_cast]
theorem coe_pow (r : ℝ≥0) (n : ℕ) : ((r ^ n : ℝ≥0) : ℝ) = (r : ℝ) ^ n := rfl

Power Preservation under Inclusion of Non-negative Reals

Informal description

For any non-negative real number $r \in \mathbb{R}_{\geq 0}$ and any natural number $n \in \mathbb{N}$, the canonical inclusion map $\mathbb{R}_{\geq 0} \to \mathbb{R}$ preserves powers, i.e., $(r^n : \mathbb{R}_{\geq 0}) = (r : \mathbb{R})^n$.

NNReal.coe_zpow theorem

(r : ℝ≥0) (n : ℤ) : ((r ^ n : ℝ≥0) : ℝ) = (r : ℝ) ^ n

Full source

@[simp, norm_cast]
theorem coe_zpow (r : ℝ≥0) (n : ℤ) : ((r ^ n : ℝ≥0) : ℝ) = (r : ℝ) ^ n := rfl

Preservation of Integer Powers under Inclusion $\mathbb{R}_{\geq 0} \to \mathbb{R}$

Informal description

For any non-negative real number $r \in \mathbb{R}_{\geq 0}$ and any integer $n \in \mathbb{Z}$, the canonical inclusion map $\mathbb{R}_{\geq 0} \to \mathbb{R}$ preserves integer powers, i.e., $(r^n : \mathbb{R}_{\geq 0}) = r^n$ as real numbers.

NNReal.coe_nsmul theorem

(r : ℝ≥0) (n : ℕ) : ↑(n • r) = n • (r : ℝ)

Full source

@[simp, norm_cast] lemma coe_nsmul (r : ℝ≥0) (n : ℕ) : ↑(n • r) = n • (r : ℝ) := rfl

Compatibility of Natural Scalar Multiplication with Inclusion: $\uparrow(n \cdot r) = n \cdot (\uparrow r)$

Informal description

For any non-negative real number $r \in \mathbb{R}_{\geq 0}$ and any natural number $n \in \mathbb{N}$, the scalar multiplication $n \cdot r$ in $\mathbb{R}_{\geq 0}$ coincides with the scalar multiplication $n \cdot r$ in $\mathbb{R}$ when viewed through the canonical inclusion map. In other words, $\uparrow(n \cdot r) = n \cdot (\uparrow r)$, where $\uparrow$ denotes the inclusion of $\mathbb{R}_{\geq 0}$ into $\mathbb{R}$.

NNReal.coe_nnqsmul theorem

(q : ℚ≥0) (x : ℝ≥0) : ↑(q • x) = (q • x : ℝ)

Full source

@[simp, norm_cast] lemma coe_nnqsmul (q : ℚ≥0) (x : ℝ≥0) : ↑(q • x) = (q • x : ℝ) := rfl

Scalar Multiplication Compatibility: $\mathbb{R}_{\geq 0}$ to $\mathbb{R}$ for Nonnegative Rationals

Informal description

For any nonnegative rational number $q$ and any nonnegative real number $x$, the canonical inclusion map $\mathbb{R}_{\geq 0} \to \mathbb{R}$ maps the scalar multiplication $q \cdot x$ in $\mathbb{R}_{\geq 0}$ to the scalar multiplication $q \cdot x$ in $\mathbb{R}$.

NNReal.coe_natCast theorem

(n : ℕ) : (↑(↑n : ℝ≥0) : ℝ) = n

Full source

@[simp, norm_cast]
protected theorem coe_natCast (n : ℕ) : (↑(↑n : ℝ≥0) : ℝ) = n :=
  map_natCast toRealHom n

Inclusion Preserves Natural Numbers: $\uparrow(n) = n$

Informal description

For any natural number $n$, the canonical inclusion map from non-negative real numbers to real numbers preserves the natural number $n$, i.e., $\uparrow(n) = n$ where $\uparrow$ denotes the inclusion $\mathbb{R}_{\geq 0} \hookrightarrow \mathbb{R}$.

NNReal.coe_ofNat theorem

(n : ℕ) [n.AtLeastTwo] : ((ofNat(n) : ℝ≥0) : ℝ) = ofNat(n)

Full source

@[simp, norm_cast]
protected theorem coe_ofNat (n : ℕ) [n.AtLeastTwo] : ((ofNat(n) : ℝ≥0) : ℝ) = ofNat(n) :=
  rfl

Inclusion Preserves Numerals $\geq 2$ in Non-Negative Reals

Informal description

For any natural number $n \geq 2$, the canonical inclusion map from non-negative real numbers to real numbers preserves the numeral representation, i.e., the inclusion of $n$ in $\mathbb{R}_{\geq 0}$ is equal to $n$ in $\mathbb{R}$.

NNReal.coe_ofScientific theorem

 (m : ℕ) (s : Bool) (e : ℕ) : ↑(OfScientific.ofScientific m s e : ℝ≥0) = (OfScientific.ofScientific m s e : ℝ)

Full source

@[simp, norm_cast]
protected theorem coe_ofScientific (m : ℕ) (s : Bool) (e : ℕ) :
    ↑(OfScientific.ofScientific m s e : ℝ≥0) = (OfScientific.ofScientific m s e : ℝ) :=
  rfl

Inclusion Preserves Scientific Notation for Non-Negative Reals

Informal description

For any natural numbers $m$ and $e$, and boolean $s$, the canonical inclusion map from non-negative real numbers to real numbers preserves the scientific notation representation. That is, the inclusion of $\text{OfScientific.ofScientific}~m~s~e$ in $\mathbb{R}_{\geq 0}$ is equal to $\text{OfScientific.ofScientific}~m~s~e$ in $\mathbb{R}$.

NNReal.algebraMap_eq_coe theorem

: (algebraMap ℝ≥0 ℝ : ℝ≥0 → ℝ) = (↑)

Full source

@[simp, norm_cast]
lemma algebraMap_eq_coe : (algebraMap ℝ≥0 ℝ : ℝ≥0 → ℝ) = (↑) := rfl

Algebra Map Equals Inclusion for Non-Negative Reals

Informal description

The algebra map from the non-negative real numbers $\mathbb{R}_{\geq 0}$ to the real numbers $\mathbb{R}$ coincides with the canonical inclusion map, i.e., for any $x \in \mathbb{R}_{\geq 0}$, we have $\text{algebraMap}_{\mathbb{R}_{\geq 0} \to \mathbb{R}}(x) = x$.

NNReal.coe_le_coe theorem

: (r₁ : ℝ) ≤ r₂ ↔ r₁ ≤ r₂

Full source

@[simp, norm_cast] lemma coe_le_coe : (r₁ : ℝ) ≤ r₂ ↔ r₁ ≤ r₂ := Iff.rfl

Preservation of Inequality under Inclusion of Non-Negative Reals

Informal description

For any two non-negative real numbers $r_1$ and $r_2$ in $\mathbb{R}_{\geq 0}$, the canonical inclusion map satisfies $r_1 \leq r_2$ if and only if the underlying real numbers satisfy $r_1 \leq r_2$.

NNReal.coe_lt_coe theorem

: (r₁ : ℝ) < r₂ ↔ r₁ < r₂

Full source

@[simp, norm_cast] lemma coe_lt_coe : (r₁ : ℝ) < r₂ ↔ r₁ < r₂ := Iff.rfl

Preservation of Strict Inequality under Inclusion of Non-Negative Reals

Informal description

For any two non-negative real numbers $r_1$ and $r_2$ in $\mathbb{R}_{\geq 0}$, the canonical inclusion map satisfies $r_1 < r_2$ if and only if the underlying real numbers satisfy $r_1 < r_2$.

NNReal.coe_pos theorem

: (0 : ℝ) < r ↔ 0 < r

Full source

@[simp, norm_cast] lemma coe_pos : (0 : ℝ) < r ↔ 0 < r := Iff.rfl

Positivity Preservation under Inclusion of Non-Negative Reals

Informal description

For any non-negative real number $r \in \mathbb{R}_{\geq 0}$, the canonical inclusion map satisfies $0 < r$ if and only if the underlying real number satisfies $0 < r$.

NNReal.one_le_coe theorem

: 1 ≤ (r : ℝ) ↔ 1 ≤ r

Full source

@[simp, norm_cast] lemma one_le_coe : 1 ≤ (r : ℝ) ↔ 1 ≤ r := by rw [← coe_le_coe, coe_one]

Inequality Preservation: $1 \leq r$ in $\mathbb{R}_{\geq 0}$ iff $1 \leq r$ in $\mathbb{R}$

Informal description

For any non-negative real number $r \in \mathbb{R}_{\geq 0}$, the inequality $1 \leq r$ holds in $\mathbb{R}_{\geq 0}$ if and only if the corresponding inequality $1 \leq r$ holds in $\mathbb{R}$.

NNReal.one_lt_coe theorem

: 1 < (r : ℝ) ↔ 1 < r

Full source

@[simp, norm_cast] lemma one_lt_coe : 1 < (r : ℝ) ↔ 1 < r := by rw [← coe_lt_coe, coe_one]

Preservation of Strict Inequality for One under Inclusion of Non-Negative Reals

Informal description

For any non-negative real number $r \in \mathbb{R}_{\geq 0}$, the inequality $1 < r$ holds if and only if the underlying real number satisfies $1 < r$.

NNReal.coe_le_one theorem

: (r : ℝ) ≤ 1 ↔ r ≤ 1

Full source

@[simp, norm_cast] lemma coe_le_one : (r : ℝ) ≤ 1 ↔ r ≤ 1 := by rw [← coe_le_coe, coe_one]

Inclusion Preserves Inequality with One in Non-Negative Reals

Informal description

For any non-negative real number $r \in \mathbb{R}_{\geq 0}$, the underlying real number $r$ is less than or equal to $1$ if and only if $r \leq 1$ in $\mathbb{R}_{\geq 0}$.

NNReal.coe_lt_one theorem

: (r : ℝ) < 1 ↔ r < 1

Full source

@[simp, norm_cast] lemma coe_lt_one : (r : ℝ) < 1 ↔ r < 1 := by rw [← coe_lt_coe, coe_one]

Inclusion Preserves Strict Inequality with One in Non-Negative Reals

Informal description

For any non-negative real number $r \in \mathbb{R}_{\geq 0}$, the canonical inclusion map satisfies $r < 1$ if and only if the underlying real number satisfies $r < 1$.

NNReal.coe_mono theorem

: Monotone ((↑) : ℝ≥0 → ℝ)

Full source

@[mono] lemma coe_mono : Monotone ((↑) : ℝ≥0 → ℝ) := fun _ _ => NNReal.coe_le_coe.2

Monotonicity of the Inclusion from Non-Negative Reals to Reals

Informal description

The canonical inclusion map from non-negative real numbers $\mathbb{R}_{\geq 0}$ to real numbers $\mathbb{R}$ is monotone. That is, for any $r_1, r_2 \in \mathbb{R}_{\geq 0}$, if $r_1 \leq r_2$ in $\mathbb{R}_{\geq 0}$, then $r_1 \leq r_2$ in $\mathbb{R}$.

Real.toNNReal_mono theorem

: Monotone Real.toNNReal

Full source

protected theorem _root_.Real.toNNReal_mono : Monotone Real.toNNReal := fun _ _ h =>
  max_le_max h (le_refl 0)

Monotonicity of the Non-Negative Part Function on Real Numbers

Informal description

The function $\operatorname{toNNReal} : \mathbb{R} \to \mathbb{R}_{\geq 0}$, defined by $\operatorname{toNNReal}(x) = \max(x, 0)$, is monotone. That is, for any real numbers $x$ and $y$, if $x \leq y$, then $\operatorname{toNNReal}(x) \leq \operatorname{toNNReal}(y)$.

Real.toNNReal_coe theorem

{r : ℝ≥0} : Real.toNNReal r = r

Full source

@[simp]
theorem _root_.Real.toNNReal_coe {r : ℝ≥0} : Real.toNNReal r = r :=
  NNReal.eq <| max_eq_left r.2

Non-negative part preserves non-negative real numbers

Informal description

For any non-negative real number $r \in \mathbb{R}_{\geq 0}$, the non-negative part of $r$ (obtained via `Real.toNNReal`) is equal to $r$ itself, i.e., $\text{toNNReal}(r) = r$.

NNReal.mk_natCast theorem

(n : ℕ) : @Eq ℝ≥0 (⟨(n : ℝ), n.cast_nonneg⟩ : ℝ≥0) n

Full source

@[simp]
theorem mk_natCast (n : ℕ) : @Eq ℝ≥0 (⟨(n : ℝ), n.cast_nonneg⟩ : ℝ≥0) n :=
  NNReal.eq (NNReal.coe_natCast n).symm

Canonical embedding of natural numbers into non-negative reals preserves equality

Informal description

For any natural number $n$, the non-negative real number constructed from the real number $n$ (via the canonical embedding $\mathbb{N} \to \mathbb{R}$) and the proof that $n \geq 0$ is equal to the natural number $n$ itself when viewed as an element of $\mathbb{R}_{\geq 0}$.

Real.toNNReal_coe_nat theorem

(n : ℕ) : Real.toNNReal n = n

Full source

@[simp]
theorem _root_.Real.toNNReal_coe_nat (n : ℕ) : Real.toNNReal n = n :=
  NNReal.eq <| by simp [Real.coe_toNNReal]

Non-negative part preserves natural numbers: $\text{toNNReal}(n) = n$

Informal description

For any natural number $n$, the non-negative part of $n$ (as a real number) is equal to $n$ itself, i.e., $\text{toNNReal}(n) = n$.

Real.toNNReal_ofNat theorem

(n : ℕ) [n.AtLeastTwo] : Real.toNNReal ofNat(n) = OfNat.ofNat n

Full source

@[simp]
theorem _root_.Real.toNNReal_ofNat (n : ℕ) [n.AtLeastTwo] :
    Real.toNNReal ofNat(n) = OfNat.ofNat n :=
  Real.toNNReal_coe_nat n

Non-negative part preserves numerals $\geq 2$: $\text{toNNReal}(n) = n$ for $n \geq 2$

Informal description

For any natural number $n \geq 2$, the non-negative part of $n$ (as a real number) is equal to $n$ itself when interpreted as an element of $\mathbb{R}_{\geq 0}$, i.e., $\text{toNNReal}(n) = n$.

NNReal.gi definition

: GaloisInsertion Real.toNNReal (↑)

Full source

/-- `Real.toNNReal` and `NNReal.toReal : ℝ≥0 → ℝ` form a Galois insertion. -/
def gi : GaloisInsertion Real.toNNReal (↑) :=
  GaloisInsertion.monotoneIntro NNReal.coe_mono Real.toNNReal_mono Real.le_coe_toNNReal fun _ =>
    Real.toNNReal_coe

Galois insertion between real numbers and their non-negative parts

Informal description

The pair of functions `Real.toNNReal` (which maps a real number to its non-negative part, defined as $\max(x, 0)$) and the canonical inclusion map from non-negative real numbers to real numbers form a Galois insertion. Specifically: 1. Both functions are monotone. 2. For any real number $r$, $r \leq \text{toNNReal}(r)$. 3. For any non-negative real number $x \in \mathbb{R}_{\geq 0}$, $\text{toNNReal}(x) = x$. This means that `Real.toNNReal` is a retraction of the inclusion map, and the inclusion map is a section of `Real.toNNReal`.

NNReal.instPosSMulStrictMono instance

{α} [Preorder α] [MulAction ℝ α] [PosSMulStrictMono ℝ α] : PosSMulStrictMono ℝ≥0 α

Full source

instance instPosSMulStrictMono {α} [Preorder α] [MulAction ℝ α] [PosSMulStrictMono ℝ α] :
    PosSMulStrictMono ℝ≥0 α where
  elim _r hr _a₁ _a₂ ha := (smul_lt_smul_of_pos_left ha (coe_pos.2 hr):)

Strict Monotonicity of Scalar Multiplication by Positive Non-Negative Reals

Informal description

For any preorder $\alpha$ with a multiplicative action of the real numbers $\mathbb{R}$ such that left scalar multiplication by positive real numbers is strictly monotone, the non-negative real numbers $\mathbb{R}_{\geq 0}$ also induce a strictly monotone left scalar multiplication on $\alpha$. That is, for any $a > 0$ in $\mathbb{R}_{\geq 0}$ and any $b_1 < b_2$ in $\alpha$, we have $a \cdot b_1 < a \cdot b_2$.

NNReal.instSMulPosStrictMono instance

{α} [Zero α] [Preorder α] [MulAction ℝ α] [SMulPosStrictMono ℝ α] : SMulPosStrictMono ℝ≥0 α

Full source

instance instSMulPosStrictMono {α} [Zero α] [Preorder α] [MulAction ℝ α] [SMulPosStrictMono ℝ α] :
    SMulPosStrictMono ℝ≥0 α where
  elim _a ha _r₁ _r₂ hr := (smul_lt_smul_of_pos_right (coe_lt_coe.2 hr) ha :)

Strict Monotonicity of Scalar Multiplication by Non-Negative Reals on Positive Elements

Informal description

For any type $\alpha$ with a zero element and a preorder, equipped with a multiplicative action of the real numbers $\mathbb{R}$ where scalar multiplication is strictly monotone in the left argument when the right argument is positive, the non-negative real numbers $\mathbb{R}_{\geq 0}$ also satisfy this strict monotonicity property.

NNReal.orderIsoIccZeroCoe definition

(a : ℝ≥0) : Set.Icc (0 : ℝ) a ≃o Set.Iic a

Full source

/-- If `a` is a nonnegative real number, then the closed interval `[0, a]` in `ℝ` is order
isomorphic to the interval `Set.Iic a`. -/
-- TODO: if we use `@[simps!]` it will look through the `NNReal = Subtype _` definition,
-- but if we use `@[simps]` it will not look through the `Equiv.Set.sep` definition.
-- Turning `NNReal` into a structure may be the best way to go here.
-- @[simps!? apply_coe_coe]
def orderIsoIccZeroCoe (a : ℝ≥0) : Set.IccSet.Icc (0 : ℝ) a ≃o Set.Iic a where
  toEquiv := Equiv.Set.sep (Set.Ici 0) fun x : ℝ => x ≤ a
  map_rel_iff' := Iff.rfl

Order isomorphism between $[0, a]$ and $(-\infty, a]$ for non-negative real $a$

Informal description

For any non-negative real number $ a $, the closed interval $[0, a]$ in $\mathbb{R}$ is order isomorphic to the left-infinite right-closed interval $(-\infty, a]$ (denoted as $\text{Iic } a$) via the natural inclusion map.

NNReal.orderIsoIccZeroCoe_apply_coe_coe theorem

(a : ℝ≥0) (b : Set.Icc (0 : ℝ) a) : (orderIsoIccZeroCoe a b : ℝ) = b

Full source

@[simp]
theorem orderIsoIccZeroCoe_apply_coe_coe (a : ℝ≥0) (b : Set.Icc (0 : ℝ) a) :
    (orderIsoIccZeroCoe a b : ℝ) = b :=
  rfl

Image of Interval Element under Order Isomorphism Preserves Value

Informal description

For any non-negative real number $a$ and any element $b$ in the closed interval $[0, a] \subseteq \mathbb{R}$, the image of $b$ under the order isomorphism $\text{orderIsoIccZeroCoe}(a)$ (viewed as a real number) is equal to $b$ itself.

NNReal.orderIsoIccZeroCoe_symm_apply_coe theorem

(a : ℝ≥0) (b : Set.Iic a) : ((orderIsoIccZeroCoe a).symm b : ℝ) = b

Full source

@[simp]
theorem orderIsoIccZeroCoe_symm_apply_coe (a : ℝ≥0) (b : Set.Iic a) :
    ((orderIsoIccZeroCoe a).symm b : ℝ) = b :=
  rfl

Inverse Order Isomorphism Preserves Real Value for Non-Negative Reals

Informal description

For any non-negative real number $a$ and any element $b$ in the left-infinite right-closed interval $(-\infty, a]$, the real number value of the inverse image of $b$ under the order isomorphism between $[0, a]$ and $(-\infty, a]$ is equal to $b$. In other words, if $\phi : [0, a] \simeq_o (-\infty, a]$ is the order isomorphism, then for any $b \in (-\infty, a]$, we have $\phi^{-1}(b) = b$ as real numbers.

NNReal.coe_image theorem

{s : Set ℝ≥0} : (↑) '' s = {x : ℝ | ∃ h : 0 ≤ x, @Membership.mem ℝ≥0 _ _ s ⟨x, h⟩}

Full source

theorem coe_image {s : Set ℝ≥0} :
    (↑)(↑) '' s = { x : ℝ | ∃ h : 0 ≤ x, @Membership.mem ℝ≥0 _ _ s ⟨x, h⟩ } :=
  Subtype.coe_image

Image of Non-Negative Real Subset Equals Non-Negative Elements in Reals

Informal description

For any subset $s$ of the non-negative real numbers $\mathbb{R}_{\geq 0}$, the image of $s$ under the canonical inclusion map $\mathbb{R}_{\geq 0} \to \mathbb{R}$ is equal to the set of real numbers $x$ such that $0 \leq x$ and there exists an element $\langle x, h \rangle \in s$ where $h$ is a proof that $0 \leq x$.

NNReal.bddAbove_coe theorem

{s : Set ℝ≥0} : BddAbove (((↑) : ℝ≥0 → ℝ) '' s) ↔ BddAbove s

Full source

theorem bddAbove_coe {s : Set ℝ≥0} : BddAboveBddAbove (((↑) : ℝ≥0 → ℝ) '' s) ↔ BddAbove s :=
  Iff.intro
    (fun ⟨b, hb⟩ =>
      ⟨Real.toNNReal b, fun ⟨y, _⟩ hys =>
        show y ≤ max b 0 from le_max_of_le_left <| hb <| Set.mem_image_of_mem _ hys⟩)
    fun ⟨b, hb⟩ => ⟨b, fun _ ⟨_, hx, eq⟩ => eq ▸ hb hx⟩

Bounded Above Preservation under Inclusion of Non-Negative Reals

Informal description

For any subset $s$ of the non-negative real numbers $\mathbb{R}_{\geq 0}$, the image of $s$ under the canonical inclusion map $\mathbb{R}_{\geq 0} \to \mathbb{R}$ is bounded above in $\mathbb{R}$ if and only if $s$ is bounded above in $\mathbb{R}_{\geq 0}$.

NNReal.bddBelow_coe theorem

(s : Set ℝ≥0) : BddBelow (((↑) : ℝ≥0 → ℝ) '' s)

Full source

theorem bddBelow_coe (s : Set ℝ≥0) : BddBelow (((↑) : ℝ≥0 → ℝ)((↑) : ℝ≥0 → ℝ) '' s) :=
  ⟨0, fun _ ⟨q, _, eq⟩ => eq ▸ q.2⟩

Image of Non-Negative Real Set is Bounded Below in Reals

Informal description

For any set $s$ of non-negative real numbers (i.e., $s \subseteq \mathbb{R}_{\geq 0}$), the image of $s$ under the canonical inclusion map $\mathbb{R}_{\geq 0} \to \mathbb{R}$ is bounded below in $\mathbb{R}$.

NNReal.instConditionallyCompleteLinearOrderBot instance

: ConditionallyCompleteLinearOrderBot ℝ≥0

Full source

noncomputable instance : ConditionallyCompleteLinearOrderBot ℝ≥0 :=
  Nonneg.conditionallyCompleteLinearOrderBot 0

Conditionally Complete Linear Order with Bottom on Non-Negative Reals

Informal description

The non-negative real numbers $\mathbb{R}_{\geq 0}$ form a conditionally complete linear order with a bottom element. This means that every nonempty subset of $\mathbb{R}_{\geq 0}$ that is bounded above has a supremum, and every nonempty subset (which is automatically bounded below by $0$) has an infimum. The bottom element is $0$.

NNReal.coe_sSup theorem

(s : Set ℝ≥0) : (↑(sSup s) : ℝ) = sSup (((↑) : ℝ≥0 → ℝ) '' s)

Full source

@[norm_cast]
theorem coe_sSup (s : Set ℝ≥0) : (↑(sSup s) : ℝ) = sSup (((↑) : ℝ≥0 → ℝ)((↑) : ℝ≥0 → ℝ) '' s) := by
  rcases Set.eq_empty_or_nonempty s with rfl|hs
  · simp
  by_cases H : BddAbove s
  · have A : sSupsSup (Subtype.val '' s) ∈ Set.Ici 0 := by
      apply Real.sSup_nonneg
      rintro - ⟨y, -, rfl⟩
      exact y.2
    exact (@subset_sSup_of_within ℝ (Set.Ici (0 : ℝ)) _ _ (_) s hs H A).symm
  · simp only [csSup_of_not_bddAbove H, csSup_empty, bot_eq_zero', NNReal.coe_zero]
    apply (Real.sSup_of_not_bddAbove ?_).symm
    contrapose! H
    exact bddAbove_coe.1 H

Supremum Preservation under Inclusion of Non-Negative Reals

Informal description

For any subset $s$ of the non-negative real numbers $\mathbb{R}_{\geq 0}$, the canonical inclusion map $\mathbb{R}_{\geq 0} \to \mathbb{R}$ preserves suprema, i.e., $\sup s = \sup \{x \in \mathbb{R} \mid x \in s\}$.

NNReal.coe_iSup theorem

{ι : Sort*} (s : ι → ℝ≥0) : (↑(⨆ i, s i) : ℝ) = ⨆ i, ↑(s i)

Full source

@[simp, norm_cast]
theorem coe_iSup {ι : Sort*} (s : ι → ℝ≥0) : (↑(⨆ i, s i) : ℝ) = ⨆ i, ↑(s i) := by
  rw [iSup, iSup, coe_sSup, ← Set.range_comp]; rfl

Supremum Preservation under Inclusion of Indexed Non-Negative Reals

Informal description

For any indexed family of non-negative real numbers $(s_i)_{i \in \iota}$, the canonical inclusion map $\mathbb{R}_{\geq 0} \to \mathbb{R}$ preserves suprema, i.e., \[ \left(\sup_{i} s_i\right) = \sup_{i} s_i \] where the left supremum is taken in $\mathbb{R}_{\geq 0}$ and the right supremum is taken in $\mathbb{R}$.

NNReal.coe_sInf theorem

(s : Set ℝ≥0) : (↑(sInf s) : ℝ) = sInf (((↑) : ℝ≥0 → ℝ) '' s)

Full source

@[norm_cast]
theorem coe_sInf (s : Set ℝ≥0) : (↑(sInf s) : ℝ) = sInf (((↑) : ℝ≥0 → ℝ)((↑) : ℝ≥0 → ℝ) '' s) := by
  rcases Set.eq_empty_or_nonempty s with rfl|hs
  · simp only [Set.image_empty, Real.sInf_empty, coe_eq_zero]
    exact @subset_sInf_emptyset ℝ (Set.Ici (0 : ℝ)) _ _ (_)
  have A : sInfsInf (Subtype.val '' s) ∈ Set.Ici 0 := by
    apply Real.sInf_nonneg
    rintro - ⟨y, -, rfl⟩
    exact y.2
  exact (@subset_sInf_of_within ℝ (Set.Ici (0 : ℝ)) _ _ (_) s hs (OrderBot.bddBelow s) A).symm

Infimum Preservation under Inclusion of Non-Negative Reals

Informal description

For any subset $s$ of the non-negative real numbers $\mathbb{R}_{\geq 0}$, the canonical inclusion map $\mathbb{R}_{\geq 0} \to \mathbb{R}$ preserves infima, i.e., $\inf s = \inf \{x \in \mathbb{R} \mid x \in s\}$.

NNReal.sInf_empty theorem

: sInf (∅ : Set ℝ≥0) = 0

Full source

@[simp]
theorem sInf_empty : sInf (∅ : Set ℝ≥0) = 0 := by
  rw [← coe_eq_zero, coe_sInf, Set.image_empty, Real.sInf_empty]

Infimum of Empty Set in Non-Negative Reals is Zero

Informal description

The infimum of the empty set in the non-negative real numbers $\mathbb{R}_{\geq 0}$ is equal to $0$, i.e., $\inf \emptyset = 0$.

NNReal.coe_iInf theorem

{ι : Sort*} (s : ι → ℝ≥0) : (↑(⨅ i, s i) : ℝ) = ⨅ i, ↑(s i)

Full source

@[norm_cast]
theorem coe_iInf {ι : Sort*} (s : ι → ℝ≥0) : (↑(⨅ i, s i) : ℝ) = ⨅ i, ↑(s i) := by
  rw [iInf, iInf, coe_sInf, ← Set.range_comp]; rfl

Infimum Preservation under Inclusion of Non-Negative Reals for Indexed Families

Informal description

For any indexed family of non-negative real numbers $(s_i)_{i \in \iota}$, the canonical inclusion map from $\mathbb{R}_{\geq 0}$ to $\mathbb{R}$ preserves infima, i.e., \[ \inf_{i \in \iota} s_i = \inf_{i \in \iota} s_i \] where the left infimum is taken in $\mathbb{R}_{\geq 0}$ and the right infimum is taken in $\mathbb{R}$.

NNReal.addLeftMono instance

: AddLeftMono ℝ≥0

Full source

instance addLeftMono : AddLeftMono ℝ≥0 := inferInstance

Monotonicity of Left Addition in Non-negative Reals

Informal description

For any non-negative real numbers $a, b_1, b_2 \in \mathbb{R}_{\geq 0}$, if $b_1 \leq b_2$, then $a + b_1 \leq a + b_2$. That is, left addition by any fixed non-negative real number is monotone with respect to the usual order on $\mathbb{R}_{\geq 0}$.

NNReal.addLeftReflectLT instance

: AddLeftReflectLT ℝ≥0

Full source

instance addLeftReflectLT : AddLeftReflectLT ℝ≥0 := inferInstance

Left Addition Reflects Strict Order on Non-Negative Reals

Informal description

For any non-negative real numbers $a, b_1, b_2 \in \mathbb{R}_{\geq 0}$, if $a + b_1 < a + b_2$, then $b_1 < b_2$. That is, left addition by any fixed non-negative real number reflects the strict order on $\mathbb{R}_{\geq 0}$.

NNReal.mulLeftMono instance

: MulLeftMono ℝ≥0

Full source

instance mulLeftMono : MulLeftMono ℝ≥0 := inferInstance

Monotonicity of Left Multiplication in Non-negative Reals

Informal description

For any non-negative real numbers $a, b_1, b_2 \in \mathbb{R}_{\geq 0}$, if $b_1 \leq b_2$, then $a \cdot b_1 \leq a \cdot b_2$. In other words, left multiplication by any fixed non-negative real number is monotone with respect to the usual order on $\mathbb{R}_{\geq 0}$.

NNReal.lt_iff_exists_rat_btwn theorem

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

Full source

theorem lt_iff_exists_rat_btwn (a b : ℝ≥0) :
    a < b ↔ ∃ q : ℚ, 0 ≤ q ∧ a < Real.toNNReal q ∧ Real.toNNReal q < b :=
  Iff.intro
    (fun h : (↑a : ℝ) < (↑b : ℝ) =>
      let ⟨q, haq, hqb⟩ := exists_rat_btwn h
      have : 0 ≤ (q : ℝ) := le_trans a.2 <| le_of_lt haq
      ⟨q, Rat.cast_nonneg.1 this, by
        simp [Real.coe_toNNReal _ this, NNReal.coe_lt_coe.symm, haq, hqb]⟩)
    fun ⟨_, _, haq, hqb⟩ => lt_trans haq hqb

Characterization of Strict Inequality in Non-Negative Reals via Rational Numbers: $a < b \leftrightarrow \exists q \in \mathbb{Q}_{\geq 0}, a < q < b$

Informal description

For any two non-negative real numbers $a$ and $b$ in $\mathbb{R}_{\geq 0}$, the strict inequality $a < b$ holds if and only if there exists a non-negative rational number $q$ such that $a < q$ and $q < b$ when both are considered as non-negative real numbers via the canonical embedding.

NNReal.bot_eq_zero theorem

: (⊥ : ℝ≥0) = 0

Full source

theorem bot_eq_zero : (⊥ : ℝ≥0) = 0 := rfl

Bottom Element of Non-Negative Reals is Zero: $\bot = 0$

Informal description

The bottom element of the non-negative real numbers $\mathbb{R}_{\geq 0}$ is equal to $0$, i.e., $\bot = 0$.

NNReal.mul_sup theorem

(a b c : ℝ≥0) : a * (b ⊔ c) = a * b ⊔ a * c

Full source

theorem mul_sup (a b c : ℝ≥0) : a * (b ⊔ c) = a * b ⊔ a * c :=
  mul_max_of_nonneg _ _ <| zero_le a

Distributivity of multiplication over maximum in non-negative reals: $a \cdot \max(b, c) = \max(a \cdot b, a \cdot c)$

Informal description

For any non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0}$, the multiplication by $a$ distributes over the supremum (maximum) of $b$ and $c$, i.e., \[ a \cdot \max(b, c) = \max(a \cdot b, a \cdot c). \]

NNReal.sup_mul theorem

(a b c : ℝ≥0) : (a ⊔ b) * c = a * c ⊔ b * c

Full source

theorem sup_mul (a b c : ℝ≥0) : (a ⊔ b) * c = a * c ⊔ b * c :=
  max_mul_of_nonneg _ _ <| zero_le c

Distributivity of Maximum over Multiplication in Non-Negative Reals: $\max(a, b) \cdot c = \max(a \cdot c, b \cdot c)$

Informal description

For any non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0}$, the maximum of $a$ and $b$ multiplied by $c$ is equal to the maximum of $a \cdot c$ and $b \cdot c$, i.e., \[ \max(a, b) \cdot c = \max(a \cdot c, b \cdot c). \]

NNReal.coe_max theorem

(x y : ℝ≥0) : ((max x y : ℝ≥0) : ℝ) = max (x : ℝ) (y : ℝ)

Full source

@[simp, norm_cast]
theorem coe_max (x y : ℝ≥0) : ((max x y : ℝ≥0) : ℝ) = max (x : ℝ) (y : ℝ) :=
  NNReal.coe_mono.map_max

Preservation of Maximum under Inclusion from Non-Negative Reals to Reals

Informal description

For any non-negative real numbers $x, y \in \mathbb{R}_{\geq 0}$, the canonical inclusion map preserves the maximum operation, i.e., $\max(x, y) = \max(x, y)$ as real numbers.

NNReal.coe_min theorem

(x y : ℝ≥0) : ((min x y : ℝ≥0) : ℝ) = min (x : ℝ) (y : ℝ)

Full source

@[simp, norm_cast]
theorem coe_min (x y : ℝ≥0) : ((min x y : ℝ≥0) : ℝ) = min (x : ℝ) (y : ℝ) :=
  NNReal.coe_mono.map_min

Preservation of Minimum under Inclusion from Non-Negative Reals to Reals

Informal description

For any non-negative real numbers $x, y \in \mathbb{R}_{\geq 0}$, the canonical inclusion map preserves the minimum operation, i.e., $\min(x, y) = \min(x, y)$ as real numbers.

NNReal.zero_le_coe theorem

{q : ℝ≥0} : 0 ≤ (q : ℝ)

Full source

@[simp]
theorem zero_le_coe {q : ℝ≥0} : 0 ≤ (q : ℝ) :=
  q.2

Non-negativity of the inclusion map from $\mathbb{R}_{\geq 0}$ to $\mathbb{R}$

Informal description

For any non-negative real number $q \in \mathbb{R}_{\geq 0}$, its underlying real value satisfies $0 \leq q$.

NNReal.instOrderedSMul instance

{M : Type*} [AddCommMonoid M] [PartialOrder M] [Module ℝ M] [OrderedSMul ℝ M] : OrderedSMul ℝ≥0 M

Full source

instance instOrderedSMul {M : Type*} [AddCommMonoid M] [PartialOrder M]
    [Module ℝ M] [OrderedSMul ℝ M] :
    OrderedSMul ℝ≥0 M where
  smul_lt_smul_of_pos hab hc := (smul_lt_smul_of_pos_left hab (NNReal.coe_pos.2 hc) :)
  lt_of_smul_lt_smul_of_pos {_ _ c} hab _ :=
    lt_of_smul_lt_smul_of_nonneg_left (by exact hab) (NNReal.coe_nonneg c)

Ordered Scalar Multiplication for Non-negative Real Numbers

Informal description

For any additive commutative monoid $M$ with a partial order and a module structure over the real numbers $\mathbb{R}$ that is compatible with the order (i.e., $\mathbb{R}$ acts on $M$ in an order-preserving way), $M$ also has an ordered scalar multiplication structure over the non-negative real numbers $\mathbb{R}_{\geq 0}$.

Real.coe_toNNReal' theorem

(r : ℝ) : (Real.toNNReal r : ℝ) = max r 0

Full source

@[simp]
theorem coe_toNNReal' (r : ℝ) : (Real.toNNReal r : ℝ) = max r 0 :=
  rfl

Non-negative part equals maximum with zero: $\text{toNNReal}(r) = \max(r, 0)$

Informal description

For any real number $r$, the underlying real value of its non-negative part $\text{toNNReal}(r)$ is equal to the maximum of $r$ and $0$, i.e., $\text{toNNReal}(r) = \max(r, 0)$.

Real.toNNReal_zero theorem

: Real.toNNReal 0 = 0

Full source

@[simp]
theorem toNNReal_zero : Real.toNNReal 0 = 0 := NNReal.eq <| coe_toNNReal _ le_rfl

Non-negative part of zero is zero: $\text{toNNReal}(0) = 0$

Informal description

The non-negative part of the real number $0$ is $0$, i.e., $\text{toNNReal}(0) = 0$.

Real.toNNReal_one theorem

: Real.toNNReal 1 = 1

Full source

@[simp]
theorem toNNReal_one : Real.toNNReal 1 = 1 := NNReal.eq <| coe_toNNReal _ zero_le_one

Non-negative part of one equals one: $\text{toNNReal}(1) = 1$

Informal description

The non-negative part of the real number $1$ is equal to $1$, i.e., $\text{toNNReal}(1) = 1$.

Real.toNNReal_pos theorem

{r : ℝ} : 0 < Real.toNNReal r ↔ 0 < r

Full source

@[simp]
theorem toNNReal_pos {r : ℝ} : 0 < Real.toNNReal r ↔ 0 < r := by
  simp [← NNReal.coe_lt_coe, lt_irrefl]

Positivity of Non-negative Part: $0 < \text{toNNReal}(r) \leftrightarrow 0 < r$

Informal description

For any real number $r$, the non-negative part $\text{toNNReal}(r) = \max(r, 0)$ is strictly positive if and only if $r$ is strictly positive, i.e., $0 < \text{toNNReal}(r) \leftrightarrow 0 < r$.

Real.toNNReal_eq_zero theorem

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

Full source

@[simp]
theorem toNNReal_eq_zero {r : ℝ} : Real.toNNRealReal.toNNReal r = 0 ↔ r ≤ 0 := by
  simpa [-toNNReal_pos] using not_iff_not.2 (@toNNReal_pos r)

Zero Condition for Non-negative Part: $\text{toNNReal}(r) = 0 \leftrightarrow r \leq 0$

Informal description

For any real number $r$, the non-negative part $\text{toNNReal}(r) = \max(r, 0)$ equals zero if and only if $r$ is less than or equal to zero, i.e., $\text{toNNReal}(r) = 0 \leftrightarrow r \leq 0$.

Real.toNNReal_of_nonpos theorem

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

Full source

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

Non-negative Part Vanishes for Non-positive Real Numbers

Informal description

For any real number $r$ such that $r \leq 0$, the non-negative part $\text{toNNReal}(r) = \max(r, 0)$ equals zero.

Real.toNNReal_eq_iff_eq_coe theorem

{r : ℝ} {p : ℝ≥0} (hp : p ≠ 0) : r.toNNReal = p ↔ r = p

Full source

lemma toNNReal_eq_iff_eq_coe {r : ℝ} {p : ℝ≥0} (hp : p ≠ 0) : r.toNNReal = p ↔ r = p :=
  ⟨fun h ↦ h ▸ (coe_toNNReal _ <| not_lt.1 fun hlt ↦ hp <| h ▸ toNNReal_of_nonpos hlt.le).symm,
    fun h ↦ h.symm ▸ toNNReal_coe⟩

Equivalence of Non-negative Part and Non-zero Non-negative Real Number: $\text{toNNReal}(r) = p \leftrightarrow r = p$ for $p \neq 0$

Informal description

For any real number $r$ and any non-zero non-negative real number $p \in \mathbb{R}_{\geq 0}$, the non-negative part $\text{toNNReal}(r) = \max(r, 0)$ equals $p$ if and only if $r = p$.

Real.toNNReal_eq_one theorem

{r : ℝ} : r.toNNReal = 1 ↔ r = 1

Full source

@[simp]
lemma toNNReal_eq_one {r : ℝ} : r.toNNReal = 1 ↔ r = 1 := toNNReal_eq_iff_eq_coe one_ne_zero

Equivalence of Non-negative Part and One: $\text{toNNReal}(r) = 1 \leftrightarrow r = 1$

Informal description

For any real number $r$, the non-negative part $\text{toNNReal}(r) = \max(r, 0)$ equals $1$ if and only if $r = 1$.

Real.toNNReal_eq_natCast theorem

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

Full source

@[simp]
lemma toNNReal_eq_natCast {r : ℝ} {n : ℕ} (hn : n ≠ 0) : r.toNNReal = n ↔ r = n :=
  mod_cast toNNReal_eq_iff_eq_coe <| Nat.cast_ne_zero.2 hn

Equivalence of Non-negative Part and Nonzero Natural Number: $\text{toNNReal}(r) = n \leftrightarrow r = n$ for $n \neq 0$

Informal description

For any real number $r$ and any nonzero natural number $n$, the non-negative part of $r$ equals $n$ if and only if $r$ equals $n$. That is, $\text{toNNReal}(r) = n \leftrightarrow r = n$.

Real.toNNReal_eq_ofNat theorem

{r : ℝ} {n : ℕ} [n.AtLeastTwo] : r.toNNReal = ofNat(n) ↔ r = OfNat.ofNat n

Full source

@[simp]
lemma toNNReal_eq_ofNat {r : ℝ} {n : ℕ} [n.AtLeastTwo] :
    r.toNNReal = ofNat(n) ↔ r = OfNat.ofNat n :=
  toNNReal_eq_natCast (NeZero.ne n)

Equivalence of Non-negative Part and Natural Number ≥ 2: $\text{toNNReal}(r) = n \leftrightarrow r = n$ for $n \geq 2$

Informal description

For any real number $r$ and any natural number $n \geq 2$, the non-negative part of $r$ equals $n$ if and only if $r$ equals $n$. That is, $\text{toNNReal}(r) = n \leftrightarrow r = n$.

Real.toNNReal_le_toNNReal_iff theorem

{r p : ℝ} (hp : 0 ≤ p) : toNNReal r ≤ toNNReal p ↔ r ≤ p

Full source

@[simp]
theorem toNNReal_le_toNNReal_iff {r p : ℝ} (hp : 0 ≤ p) :
    toNNRealtoNNReal r ≤ toNNReal p ↔ r ≤ p := by simp [← NNReal.coe_le_coe, hp]

Non-negative part preserves order for non-negative real numbers

Informal description

For any real numbers $r$ and $p$ with $0 \leq p$, the inequality $\text{toNNReal}(r) \leq \text{toNNReal}(p)$ holds if and only if $r \leq p$.

Real.toNNReal_le_one theorem

{r : ℝ} : r.toNNReal ≤ 1 ↔ r ≤ 1

Full source

@[simp]
lemma toNNReal_le_one {r : ℝ} : r.toNNReal ≤ 1 ↔ r ≤ 1 := by
  simpa using toNNReal_le_toNNReal_iff zero_le_one

Non-negative part inequality: $\text{toNNReal}(r) \leq 1 \leftrightarrow r \leq 1$

Informal description

For any real number $r$, the non-negative part $\text{toNNReal}(r)$ is less than or equal to $1$ if and only if $r \leq 1$.

Real.one_lt_toNNReal theorem

{r : ℝ} : 1 < r.toNNReal ↔ 1 < r

Full source

@[simp]
lemma one_lt_toNNReal {r : ℝ} : 1 < r.toNNReal ↔ 1 < r := by
  simpa only [not_le] using toNNReal_le_one.not

Strict inequality for non-negative part: $\text{toNNReal}(r) > 1 \leftrightarrow r > 1$

Informal description

For any real number $r$, the non-negative part $\text{toNNReal}(r)$ is strictly greater than $1$ if and only if $r > 1$.

Real.toNNReal_le_natCast theorem

{r : ℝ} {n : ℕ} : r.toNNReal ≤ n ↔ r ≤ n

Full source

@[simp]
lemma toNNReal_le_natCast {r : ℝ} {n : ℕ} : r.toNNReal ≤ n ↔ r ≤ n := by
  simpa using toNNReal_le_toNNReal_iff n.cast_nonneg

Non-negative part inequality with natural numbers: $\text{toNNReal}(r) \leq n \leftrightarrow r \leq n$

Informal description

For any real number $r$ and any natural number $n$, the non-negative part $\text{toNNReal}(r)$ is less than or equal to $n$ if and only if $r \leq n$.

Real.natCast_lt_toNNReal theorem

{r : ℝ} {n : ℕ} : n < r.toNNReal ↔ n < r

Full source

@[simp]
lemma natCast_lt_toNNReal {r : ℝ} {n : ℕ} : n < r.toNNReal ↔ n < r := by
  simpa only [not_le] using toNNReal_le_natCast.not

Strict inequality for non-negative part: $n < \text{toNNReal}(r) \leftrightarrow n < r$

Informal description

For any real number $r$ and any natural number $n$, the non-negative part $\text{toNNReal}(r) = \max(r, 0)$ satisfies $n < \text{toNNReal}(r)$ if and only if $n < r$.

Real.toNNReal_le_ofNat theorem

{r : ℝ} {n : ℕ} [n.AtLeastTwo] : r.toNNReal ≤ ofNat(n) ↔ r ≤ n

Full source

@[simp]
lemma toNNReal_le_ofNat {r : ℝ} {n : ℕ} [n.AtLeastTwo] :
    r.toNNReal ≤ ofNat(n) ↔ r ≤ n :=
  toNNReal_le_natCast

Non-negative part inequality with numerals ≥ 2: $\text{toNNReal}(r) \leq n \leftrightarrow r \leq n$ for $n \geq 2$

Informal description

For any real number $r$ and any natural number $n \geq 2$, the non-negative part of $r$ (i.e., $\max(r, 0)$) is less than or equal to $n$ if and only if $r \leq n$.

Real.ofNat_lt_toNNReal theorem

{r : ℝ} {n : ℕ} [n.AtLeastTwo] : ofNat(n) < r.toNNReal ↔ n < r

Full source

@[simp]
lemma ofNat_lt_toNNReal {r : ℝ} {n : ℕ} [n.AtLeastTwo] :
    ofNat(n)ofNat(n) < r.toNNReal ↔ n < r :=
  natCast_lt_toNNReal

Strict inequality between numeral ≥ 2 and non-negative part: $n < \text{toNNReal}(r) \leftrightarrow n < r$ for $n \geq 2$

Informal description

For any real number $r$ and any natural number $n \geq 2$, the non-negative part of $r$ (i.e., $\max(r, 0)$) is strictly greater than $n$ if and only if $r$ is strictly greater than $n$.

Real.toNNReal_eq_toNNReal_iff theorem

{r p : ℝ} (hr : 0 ≤ r) (hp : 0 ≤ p) : toNNReal r = toNNReal p ↔ r = p

Full source

@[simp]
theorem toNNReal_eq_toNNReal_iff {r p : ℝ} (hr : 0 ≤ r) (hp : 0 ≤ p) :
    toNNRealtoNNReal r = toNNReal p ↔ r = p := by simp [← coe_inj, coe_toNNReal, hr, hp]

Equality of Non-negative Parts of Real Numbers

Informal description

For any two real numbers $r$ and $p$ such that $0 \leq r$ and $0 \leq p$, the non-negative parts of $r$ and $p$ are equal if and only if $r = p$. In other words, $\max(r, 0) = \max(p, 0) \leftrightarrow r = p$.

Real.toNNReal_lt_toNNReal_iff' theorem

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

Full source

@[simp]
theorem toNNReal_lt_toNNReal_iff' {r p : ℝ} : Real.toNNRealReal.toNNReal r < Real.toNNReal p ↔ r < p ∧ 0 < p :=
  NNReal.coe_lt_coe.symm.trans max_lt_max_left_iff

Inequality of Non-negative Parts: $\max(r, 0) < \max(p, 0) \leftrightarrow r < p \land 0 < p$

Informal description

For any real numbers $r$ and $p$, the non-negative part of $r$ is strictly less than the non-negative part of $p$ if and only if $r$ is strictly less than $p$ and $p$ is strictly positive. In other words: \[ \max(r, 0) < \max(p, 0) \leftrightarrow r < p \land 0 < p. \]

Real.toNNReal_lt_toNNReal_iff theorem

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

Full source

theorem toNNReal_lt_toNNReal_iff {r p : ℝ} (h : 0 < p) :
    Real.toNNRealReal.toNNReal r < Real.toNNReal p ↔ r < p :=
  toNNReal_lt_toNNReal_iff'.trans (and_iff_left h)

Inequality of Non-negative Parts for Positive $p$: $\max(r, 0) < \max(p, 0) \leftrightarrow r < p$

Informal description

For any real numbers $r$ and $p$ with $p > 0$, the non-negative part of $r$ is strictly less than the non-negative part of $p$ if and only if $r < p$. In other words: \[ \max(r, 0) < \max(p, 0) \leftrightarrow r < p. \]

Real.lt_of_toNNReal_lt theorem

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

Full source

theorem lt_of_toNNReal_lt {r p : ℝ} (h : r.toNNReal < p.toNNReal) : r < p :=
  (Real.toNNReal_lt_toNNReal_iff <| Real.toNNReal_pos.1 (ne_bot_of_gt h).bot_lt).1 h

Inequality Preservation for Non-negative Parts of Real Numbers: $\max(r, 0) < \max(p, 0) \implies r < p$

Informal description

For any real numbers $r$ and $p$, if the non-negative part of $r$ is strictly less than the non-negative part of $p$, then $r$ is strictly less than $p$. In other words: \[ \max(r, 0) < \max(p, 0) \implies r < p. \]

Real.toNNReal_lt_toNNReal_iff_of_nonneg theorem

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

Full source

theorem toNNReal_lt_toNNReal_iff_of_nonneg {r p : ℝ} (hr : 0 ≤ r) :
    Real.toNNRealReal.toNNReal r < Real.toNNReal p ↔ r < p :=
  toNNReal_lt_toNNReal_iff'.trans ⟨And.left, fun h => ⟨h, lt_of_le_of_lt hr h⟩⟩

Inequality Preservation for Non-negative Parts of Non-negative Real Numbers

Informal description

For any real numbers $r$ and $p$ with $r \geq 0$, the non-negative part of $r$ is strictly less than the non-negative part of $p$ if and only if $r$ is strictly less than $p$. In other words: \[ \max(r, 0) < \max(p, 0) \leftrightarrow r < p \quad \text{when } r \geq 0. \]

Real.toNNReal_le_toNNReal_iff' theorem

{r p : ℝ} : r.toNNReal ≤ p.toNNReal ↔ r ≤ p ∨ r ≤ 0

Full source

lemma toNNReal_le_toNNReal_iff' {r p : ℝ} : r.toNNReal ≤ p.toNNReal ↔ r ≤ p ∨ r ≤ 0 := by
  simp_rw [← not_lt, toNNReal_lt_toNNReal_iff', not_and_or]

Inequality for Non-negative Parts of Real Numbers: $\max(r, 0) \leq \max(p, 0) \leftrightarrow (r \leq p \lor r \leq 0)$

Informal description

For any real numbers $r$ and $p$, the non-negative part of $r$ is less than or equal to the non-negative part of $p$ if and only if either $r \leq p$ or $r \leq 0$. In other words, $\max(r, 0) \leq \max(p, 0) \leftrightarrow (r \leq p \lor r \leq 0)$.

Real.toNNReal_le_toNNReal_iff_of_pos theorem

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

Full source

lemma toNNReal_le_toNNReal_iff_of_pos {r p : ℝ} (hr : 0 < r) : r.toNNReal ≤ p.toNNReal ↔ r ≤ p := by
  simp [toNNReal_le_toNNReal_iff', hr.not_le]

Inequality Preservation for Non-negative Parts of Positive Real Numbers

Informal description

For any real numbers $r$ and $p$ with $r > 0$, the non-negative part of $r$ is less than or equal to the non-negative part of $p$ if and only if $r \leq p$. In other words, $\max(r, 0) \leq \max(p, 0) \leftrightarrow r \leq p$ when $r > 0$.

Real.one_le_toNNReal theorem

{r : ℝ} : 1 ≤ r.toNNReal ↔ 1 ≤ r

Full source

@[simp]
lemma one_le_toNNReal {r : ℝ} : 1 ≤ r.toNNReal ↔ 1 ≤ r := by
  simpa using toNNReal_le_toNNReal_iff_of_pos one_pos

Inequality for Non-negative Part at One: $1 \leq \max(r, 0) \leftrightarrow 1 \leq r$

Informal description

For any real number $r$, the non-negative part of $r$ (i.e., $\max(r, 0)$) is greater than or equal to $1$ if and only if $r$ itself is greater than or equal to $1$.

Real.toNNReal_lt_one theorem

{r : ℝ} : r.toNNReal < 1 ↔ r < 1

Full source

@[simp]
lemma toNNReal_lt_one {r : ℝ} : r.toNNReal < 1 ↔ r < 1 := by simp only [← not_le, one_le_toNNReal]

Non-negative Part Less Than One Criterion

Informal description

For any real number $r$, the non-negative part of $r$ is less than $1$ if and only if $r$ is less than $1$. In other words, $\max(r, 0) < 1 \leftrightarrow r < 1$.

Real.natCastle_toNNReal' theorem

{n : ℕ} {r : ℝ} : ↑n ≤ r.toNNReal ↔ n ≤ r ∨ n = 0

Full source

@[simp]
lemma natCastle_toNNReal' {n : ℕ} {r : ℝ} : ↑n ≤ r.toNNReal ↔ n ≤ r ∨ n = 0 := by
  simpa [n.cast_nonneg.le_iff_eq] using toNNReal_le_toNNReal_iff' (r := n)

Comparison of Natural Number and Non-negative Part: $n \leq \max(r, 0) \leftrightarrow (n \leq r \lor n = 0)$

Informal description

For any natural number $n$ and real number $r$, the canonical embedding of $n$ into the non-negative real numbers satisfies $n \leq \max(r, 0)$ if and only if either $n \leq r$ or $n = 0$.

Real.toNNReal_lt_natCast' theorem

{n : ℕ} {r : ℝ} : r.toNNReal < n ↔ r < n ∧ n ≠ 0

Full source

@[simp]
lemma toNNReal_lt_natCast' {n : ℕ} {r : ℝ} : r.toNNReal < n ↔ r < n ∧ n ≠ 0 := by
  simpa [pos_iff_ne_zero] using toNNReal_lt_toNNReal_iff' (r := r) (p := n)

Non-negative Part Comparison with Nonzero Natural Number: $\max(r, 0) < n \leftrightarrow r < n \land n \neq 0$

Informal description

For any real number $r$ and any natural number $n$, the non-negative part of $r$ (given by $\max(r, 0)$) is strictly less than $n$ if and only if $r$ is strictly less than $n$ and $n$ is nonzero. In other words: \[ \max(r, 0) < n \leftrightarrow r < n \land n \neq 0. \]

Real.natCast_le_toNNReal theorem

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

Full source

lemma natCast_le_toNNReal {n : ℕ} {r : ℝ} (hn : n ≠ 0) : ↑n ≤ r.toNNReal ↔ n ≤ r := by simp [hn]

Comparison of Natural Number and Non-negative Part of Real Number: $n \leq \max(r, 0) \leftrightarrow n \leq r$ for $n \neq 0$

Informal description

For any natural number $n \neq 0$ and any real number $r$, the non-negative part of $r$ (given by $\max(r, 0)$) satisfies $n \leq \max(r, 0)$ if and only if $n \leq r$.

Real.toNNReal_lt_natCast theorem

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

Full source

lemma toNNReal_lt_natCast {r : ℝ} {n : ℕ} (hn : n ≠ 0) : r.toNNReal < n ↔ r < n := by simp [hn]

Comparison of Non-negative Part with Natural Number: $\max(r, 0) < n \leftrightarrow r < n$ for $n \neq 0$

Informal description

For any real number $r$ and any nonzero natural number $n$, the non-negative part of $r$ (given by $\max(r, 0)$) is less than $n$ if and only if $r$ is less than $n$.

Real.toNNReal_lt_ofNat theorem

{r : ℝ} {n : ℕ} [n.AtLeastTwo] : r.toNNReal < ofNat(n) ↔ r < OfNat.ofNat n

Full source

@[simp]
lemma toNNReal_lt_ofNat {r : ℝ} {n : ℕ} [n.AtLeastTwo] :
    r.toNNReal < ofNat(n) ↔ r < OfNat.ofNat n :=
  toNNReal_lt_natCast (NeZero.ne n)

Comparison of Non-negative Part with Numerals ≥ 2: $\max(r, 0) < n \leftrightarrow r < n$ for $n \geq 2$

Informal description

For any real number $r$ and any natural number $n \geq 2$, the non-negative part of $r$ (given by $\max(r, 0)$) is less than $n$ if and only if $r$ is less than $n$.

Real.ofNat_le_toNNReal theorem

{n : ℕ} {r : ℝ} [n.AtLeastTwo] : ofNat(n) ≤ r.toNNReal ↔ OfNat.ofNat n ≤ r

Full source

@[simp]
lemma ofNat_le_toNNReal {n : ℕ} {r : ℝ} [n.AtLeastTwo] :
    ofNat(n)ofNat(n) ≤ r.toNNReal ↔ OfNat.ofNat n ≤ r :=
  natCast_le_toNNReal (NeZero.ne n)

Comparison of Natural Number and Non-negative Part: $n \leq \max(r, 0) \leftrightarrow n \leq r$ for $n \geq 2$

Informal description

For any natural number $n \geq 2$ and any real number $r$, the non-negative part of $r$ (given by $\max(r, 0)$) satisfies $n \leq \max(r, 0)$ if and only if $n \leq r$.

Real.toNNReal_add theorem

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

Full source

@[simp]
theorem toNNReal_add {r p : ℝ} (hr : 0 ≤ r) (hp : 0 ≤ p) :
    Real.toNNReal (r + p) = Real.toNNReal r + Real.toNNReal p :=
  NNReal.eq <| by simp [hr, hp, add_nonneg]

Additivity of Non-Negative Part for Non-Negative Reals: $\operatorname{toNNReal}(r + p) = \operatorname{toNNReal}(r) + \operatorname{toNNReal}(p)$

Informal description

For any non-negative real numbers $r$ and $p$ (i.e., $r \geq 0$ and $p \geq 0$), the non-negative part of their sum equals the sum of their non-negative parts, i.e., $\operatorname{toNNReal}(r + p) = \operatorname{toNNReal}(r) + \operatorname{toNNReal}(p)$.

Real.toNNReal_add_toNNReal theorem

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

Full source

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

Additivity of Non-Negative Part Function for Non-Negative Reals: $\operatorname{toNNReal}(r) + \operatorname{toNNReal}(p) = \operatorname{toNNReal}(r + p)$

Informal description

For any non-negative real numbers $r$ and $p$ (i.e., $r \geq 0$ and $p \geq 0$), the sum of their non-negative parts equals the non-negative part of their sum, i.e., $\operatorname{toNNReal}(r) + \operatorname{toNNReal}(p) = \operatorname{toNNReal}(r + p)$.

Real.toNNReal_le_toNNReal theorem

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

Full source

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

Monotonicity of the Non-Negative Part Function: $\operatorname{toNNReal}(r) \leq \operatorname{toNNReal}(p)$ when $r \leq p$

Informal description

For any real numbers $r$ and $p$ such that $r \leq p$, the non-negative part of $r$ is less than or equal to the non-negative part of $p$, i.e., $\operatorname{toNNReal}(r) \leq \operatorname{toNNReal}(p)$.

Real.toNNReal_add_le theorem

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

Full source

theorem toNNReal_add_le {r p : ℝ} : Real.toNNReal (r + p) ≤ Real.toNNReal r + Real.toNNReal p :=
  NNReal.coe_le_coe.1 <| max_le (add_le_add (le_max_left _ _) (le_max_left _ _)) NNReal.zero_le_coe

Subadditivity of the non-negative part function: $\operatorname{toNNReal}(r + p) \leq \operatorname{toNNReal}(r) + \operatorname{toNNReal}(p)$

Informal description

For any real numbers $r$ and $p$, the non-negative part of their sum satisfies $\operatorname{toNNReal}(r + p) \leq \operatorname{toNNReal}(r) + \operatorname{toNNReal}(p)$, where $\operatorname{toNNReal}(x) = \max(x, 0)$.

Real.toNNReal_le_iff_le_coe theorem

{r : ℝ} {p : ℝ≥0} : toNNReal r ≤ p ↔ r ≤ ↑p

Full source

theorem toNNReal_le_iff_le_coe {r : ℝ} {p : ℝ≥0} : toNNRealtoNNReal r ≤ p ↔ r ≤ ↑p :=
  NNReal.gi.gc r p

Inequality Characterization for Non-Negative Part: $\operatorname{toNNReal}(r) \leq p \leftrightarrow r \leq p$

Informal description

For any real number $r$ and any non-negative real number $p \in \mathbb{R}_{\geq 0}$, the inequality $\operatorname{toNNReal}(r) \leq p$ holds if and only if $r \leq p$ (where $p$ is considered as a real number via the canonical inclusion).

Real.le_toNNReal_iff_coe_le theorem

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

Full source

theorem le_toNNReal_iff_coe_le {r : ℝ≥0} {p : ℝ} (hp : 0 ≤ p) : r ≤ Real.toNNReal p ↔ ↑r ≤ p := by
  rw [← NNReal.coe_le_coe, Real.coe_toNNReal p hp]

Inequality Characterization for Non-Negative Real Numbers: $r \leq \text{toNNReal}(p) \leftrightarrow \uparrow r \leq p$

Informal description

For a non-negative real number $r \in \mathbb{R}_{\geq 0}$ and a real number $p \in \mathbb{R}$ with $0 \leq p$, the inequality $r \leq \text{toNNReal}(p)$ holds if and only if the underlying real number of $r$ satisfies $\uparrow r \leq p$.

Real.le_toNNReal_iff_coe_le' theorem

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

Full source

theorem le_toNNReal_iff_coe_le' {r : ℝ≥0} {p : ℝ} (hr : 0 < r) : r ≤ Real.toNNReal p ↔ ↑r ≤ p :=
  (le_or_lt 0 p).elim le_toNNReal_iff_coe_le fun hp => by
    simp only [(hp.trans_le r.coe_nonneg).not_le, toNNReal_eq_zero.2 hp.le, hr.not_le]

Inequality Characterization for Positive Non-Negative Real Numbers: $r \leq \operatorname{toNNReal}(p) \leftrightarrow r \leq p$

Informal description

For any positive non-negative real number $r \in \mathbb{R}_{\geq 0}$ (i.e., $r > 0$) and any real number $p \in \mathbb{R}$, the inequality $r \leq \operatorname{toNNReal}(p)$ holds if and only if the underlying real number of $r$ satisfies $r \leq p$.

Real.toNNReal_lt_iff_lt_coe theorem

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

Full source

theorem toNNReal_lt_iff_lt_coe {r : ℝ} {p : ℝ≥0} (ha : 0 ≤ r) : Real.toNNRealReal.toNNReal r < p ↔ r < ↑p := by
  rw [← NNReal.coe_lt_coe, Real.coe_toNNReal r ha]

Comparison of Non-Negative Part with Non-Negative Real Number: $\text{toNNReal}(r) < p \leftrightarrow r < p$

Informal description

For any real number $r$ with $0 \leq r$ and any non-negative real number $p \in \mathbb{R}_{\geq 0}$, the inequality $\text{toNNReal}(r) < p$ holds if and only if $r < p$.

Real.lt_toNNReal_iff_coe_lt theorem

{r : ℝ≥0} {p : ℝ} : r < Real.toNNReal p ↔ ↑r < p

Full source

theorem lt_toNNReal_iff_coe_lt {r : ℝ≥0} {p : ℝ} : r < Real.toNNReal p ↔ ↑r < p :=
  lt_iff_lt_of_le_iff_le toNNReal_le_iff_le_coe

Inequality Characterization for Non-Negative Part: $r < \operatorname{toNNReal}(p) \leftrightarrow r < p$

Informal description

For any non-negative real number $r \in \mathbb{R}_{\geq 0}$ and any real number $p \in \mathbb{R}$, the inequality $r < \operatorname{toNNReal}(p)$ holds if and only if $r < p$ (where $r$ is considered as a real number via the canonical inclusion).

Real.toNNReal_pow theorem

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

Full source

theorem toNNReal_pow {x : ℝ} (hx : 0 ≤ x) (n : ℕ) : (x ^ n).toNNReal = x.toNNReal ^ n := by
  rw [← coe_inj, NNReal.coe_pow, Real.coe_toNNReal _ (pow_nonneg hx _),
    Real.coe_toNNReal x hx]

Power Preservation under Non-negative Part Operation: $\text{toNNReal}(x^n) = (\text{toNNReal}(x))^n$ for $x \geq 0$

Informal description

For any real number $x$ with $x \geq 0$ and any natural number $n$, the non-negative part of $x^n$ equals the $n$-th power of the non-negative part of $x$, i.e., \[ \text{toNNReal}(x^n) = (\text{toNNReal}(x))^n. \]

Real.toNNReal_zpow theorem

{x : ℝ} (hx : 0 ≤ x) (n : ℤ) : (x ^ n).toNNReal = x.toNNReal ^ n

Full source

theorem toNNReal_zpow {x : ℝ} (hx : 0 ≤ x) (n : ℤ) : (x ^ n).toNNReal = x.toNNReal ^ n := by
  rw [← coe_inj, NNReal.coe_zpow, Real.coe_toNNReal _ (zpow_nonneg hx _), Real.coe_toNNReal x hx]

Preservation of integer powers under $\operatorname{toNNReal}$ for non-negative reals

Informal description

For any real number $x \geq 0$ and any integer $n$, the non-negative part of $x^n$ equals the $n$-th power of the non-negative part of $x$, i.e., \[ \operatorname{toNNReal}(x^n) = (\operatorname{toNNReal} x)^n. \]

Real.toNNReal_mul theorem

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

Full source

theorem toNNReal_mul {p q : ℝ} (hp : 0 ≤ p) :
    Real.toNNReal (p * q) = Real.toNNReal p * Real.toNNReal q :=
  NNReal.eq <| by simp [mul_max_of_nonneg, hp]

Multiplicativity of Non-negative Part for Non-negative Real Numbers

Informal description

For any real numbers $p$ and $q$ with $p \geq 0$, the non-negative part of the product $p \cdot q$ equals the product of the non-negative parts of $p$ and $q$, i.e., \[ \text{toNNReal}(p \cdot q) = \text{toNNReal}(p) \cdot \text{toNNReal}(q). \]

NNReal.mul_eq_mul_left theorem

{a b c : ℝ≥0} (h : a ≠ 0) : a * b = a * c ↔ b = c

Full source

theorem mul_eq_mul_left {a b c : ℝ≥0} (h : a ≠ 0) : a * b = a * c ↔ b = c := by
  rw [mul_eq_mul_left_iff, or_iff_left h]

Left Cancellation Property for Multiplication in Non-Negative Real Numbers

Informal description

For any non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0}$ with $a \neq 0$, the equality $a \cdot b = a \cdot c$ holds if and only if $b = c$.

NNReal.pow_antitone_exp theorem

{a : ℝ≥0} (m n : ℕ) (mn : m ≤ n) (a1 : a ≤ 1) : a ^ n ≤ a ^ m

Full source

theorem pow_antitone_exp {a : ℝ≥0} (m n : ℕ) (mn : m ≤ n) (a1 : a ≤ 1) : a ^ n ≤ a ^ m :=
  pow_le_pow_of_le_one (zero_le a) a1 mn

Antitonicity of Powers for $0 \leq a \leq 1$: $a^n \leq a^m$ when $m \leq n$

Informal description

For any non-negative real number $a \in \mathbb{R}_{\geq 0}$ such that $a \leq 1$, and for any natural numbers $m \leq n$, the inequality $a^n \leq a^m$ holds.

NNReal.exists_pow_lt_of_lt_one theorem

{a b : ℝ≥0} (ha : 0 < a) (hb : b < 1) : ∃ n : ℕ, b ^ n < a

Full source

nonrec theorem exists_pow_lt_of_lt_one {a b : ℝ≥0} (ha : 0 < a) (hb : b < 1) :
    ∃ n : ℕ, b ^ n < a := by
  simpa only [← coe_pow, NNReal.coe_lt_coe] using
    exists_pow_lt_of_lt_one (NNReal.coe_pos.2 ha) (NNReal.coe_lt_coe.2 hb)

Existence of Power Below Positive Element in Non-Negative Reals: $b^n < a$ for $0 < a$ and $b < 1$

Informal description

For any positive non-negative real number $a > 0$ and any non-negative real number $b < 1$, there exists a natural number $n$ such that $b^n < a$.

NNReal.exists_mem_Ico_zpow theorem

{x : ℝ≥0} {y : ℝ≥0} (hx : x ≠ 0) (hy : 1 < y) : ∃ n : ℤ, x ∈ Set.Ico (y ^ n) (y ^ (n + 1))

Full source

nonrec theorem exists_mem_Ico_zpow {x : ℝ≥0} {y : ℝ≥0} (hx : x ≠ 0) (hy : 1 < y) :
    ∃ n : ℤ, x ∈ Set.Ico (y ^ n) (y ^ (n + 1)) :=
  exists_mem_Ico_zpow hx.bot_lt hy

Existence of Integer Power Interval for Nonzero Non-Negative Reals: $x \in [y^n, y^{n+1})$ for $x \neq 0$, $y > 1$

Informal description

For any nonzero non-negative real number $x \in \mathbb{R}_{\geq 0}$ and any $y \in \mathbb{R}_{\geq 0}$ with $y > 1$, there exists an integer $n$ such that $x$ lies in the interval $[y^n, y^{n+1})$.

NNReal.exists_mem_Ioc_zpow theorem

{x : ℝ≥0} {y : ℝ≥0} (hx : x ≠ 0) (hy : 1 < y) : ∃ n : ℤ, x ∈ Set.Ioc (y ^ n) (y ^ (n + 1))

Full source

nonrec theorem exists_mem_Ioc_zpow {x : ℝ≥0} {y : ℝ≥0} (hx : x ≠ 0) (hy : 1 < y) :
    ∃ n : ℤ, x ∈ Set.Ioc (y ^ n) (y ^ (n + 1)) :=
  exists_mem_Ioc_zpow hx.bot_lt hy

Existence of Integer Power Interval for Nonzero Non-Negative Reals: $x \in (y^n, y^{n+1}]$ for $x \neq 0$, $y > 1$

Informal description

For any nonzero non-negative real number $x \neq 0$ and any $y > 1$ in $\mathbb{R}_{\geq 0}$, there exists an integer $n$ such that $x$ lies in the interval $(y^n, y^{n+1}]$.

NNReal.sub_def theorem

{r p : ℝ≥0} : r - p = Real.toNNReal (r - p)

Full source

theorem sub_def {r p : ℝ≥0} : r - p = Real.toNNReal (r - p) :=
  rfl

Subtraction in Non-Negative Reals as Non-Negative Part of Real Difference

Informal description

For any two non-negative real numbers $r$ and $p$, their subtraction $r - p$ in $\mathbb{R}_{\geq 0}$ is equal to the non-negative part of their difference in $\mathbb{R}$, i.e., $r - p = \text{Real.toNNReal}(r - p)$.

NNReal.coe_sub_def theorem

{r p : ℝ≥0} : ↑(r - p) = max (r - p : ℝ) 0

Full source

theorem coe_sub_def {r p : ℝ≥0} : ↑(r - p) = max (r - p : ℝ) 0 :=
  rfl

Canonical Inclusion of Non-Negative Real Difference Equals Maximum with Zero

Informal description

For any non-negative real numbers $r$ and $p$, the canonical inclusion of their difference $r - p$ into the real numbers is equal to the maximum of $(r - p)$ and $0$, i.e., $\uparrow(r - p) = \max(r - p, 0)$.

NNReal.inv_le theorem

{r p : ℝ≥0} (h : r ≠ 0) : r⁻¹ ≤ p ↔ 1 ≤ r * p

Full source

@[simp]
theorem inv_le {r p : ℝ≥0} (h : r ≠ 0) : r⁻¹r⁻¹ ≤ p ↔ 1 ≤ r * p := by
  rw [← mul_le_mul_left (pos_iff_ne_zero.2 h), mul_inv_cancel₀ h]

Inverse Inequality for Non-Negative Reals: $r^{-1} \leq p \leftrightarrow 1 \leq r \cdot p$ when $r \neq 0$

Informal description

For any non-negative real numbers $r$ and $p$ with $r \neq 0$, the inequality $r^{-1} \leq p$ holds if and only if $1 \leq r \cdot p$.

NNReal.inv_le_of_le_mul theorem

{r p : ℝ≥0} (h : 1 ≤ r * p) : r⁻¹ ≤ p

Full source

theorem inv_le_of_le_mul {r p : ℝ≥0} (h : 1 ≤ r * p) : r⁻¹ ≤ p := by
  by_cases r = 0 <;> simp [*, inv_le]

Inverse Bound for Non-negative Reals: $1 \leq rp$ implies $r^{-1} \leq p$

Informal description

For any two non-negative real numbers $r$ and $p$, if $1 \leq r \cdot p$, then the multiplicative inverse of $r$ is less than or equal to $p$, i.e., $r^{-1} \leq p$.

NNReal.le_inv_iff_mul_le theorem

{r p : ℝ≥0} (h : p ≠ 0) : r ≤ p⁻¹ ↔ r * p ≤ 1

Full source

@[simp]
theorem le_inv_iff_mul_le {r p : ℝ≥0} (h : p ≠ 0) : r ≤ p⁻¹ ↔ r * p ≤ 1 := by
  rw [← mul_le_mul_left (pos_iff_ne_zero.2 h), mul_inv_cancel₀ h, mul_comm]

Inequality Relating Reciprocal and Product in Non-Negative Reals: $r \leq p^{-1} \leftrightarrow r \cdot p \leq 1$

Informal description

For any two non-negative real numbers $r$ and $p$ with $p \neq 0$, the inequality $r \leq p^{-1}$ holds if and only if $r \cdot p \leq 1$.

NNReal.lt_inv_iff_mul_lt theorem

{r p : ℝ≥0} (h : p ≠ 0) : r < p⁻¹ ↔ r * p < 1

Full source

@[simp]
theorem lt_inv_iff_mul_lt {r p : ℝ≥0} (h : p ≠ 0) : r < p⁻¹ ↔ r * p < 1 := by
  rw [← mul_lt_mul_left (pos_iff_ne_zero.2 h), mul_inv_cancel₀ h, mul_comm]

Inequality for Reciprocal and Product in Non-negative Reals: $r < p^{-1} \leftrightarrow r \cdot p < 1$

Informal description

For any two non-negative real numbers $r$ and $p$ with $p \neq 0$, the inequality $r < p^{-1}$ holds if and only if $r \cdot p < 1$.

NNReal.div_le_of_le_mul theorem

{a b c : ℝ≥0} (h : a ≤ b * c) : a / c ≤ b

Full source

theorem div_le_of_le_mul {a b c : ℝ≥0} (h : a ≤ b * c) : a / c ≤ b :=
  if h0 : c = 0 then by simp [h0] else (div_le_iff₀ (pos_iff_ne_zero.2 h0)).2 h

Division Inequality for Non-Negative Reals: $\frac{a}{c} \leq b$ when $a \leq b \cdot c$

Informal description

For any non-negative real numbers $a, b, c$, if $a \leq b \cdot c$, then $\frac{a}{c} \leq b$.

NNReal.div_le_of_le_mul' theorem

{a b c : ℝ≥0} (h : a ≤ b * c) : a / b ≤ c

Full source

theorem div_le_of_le_mul' {a b c : ℝ≥0} (h : a ≤ b * c) : a / b ≤ c :=
  div_le_of_le_mul <| mul_comm b c ▸ h

Division Inequality for Non-Negative Reals: $\frac{a}{b} \leq c$ when $a \leq b \cdot c$

Informal description

For any non-negative real numbers $a, b, c$, if $a \leq b \cdot c$, then $\frac{a}{b} \leq c$.

NNReal.mul_lt_of_lt_div theorem

{a b r : ℝ≥0} (h : a < b / r) : a * r < b

Full source

theorem mul_lt_of_lt_div {a b r : ℝ≥0} (h : a < b / r) : a * r < b :=
  (lt_div_iff₀ <| pos_iff_ne_zero.2 fun hr => False.elim <| by simp [hr] at h).1 h

Multiplication Inequality for Non-Negative Reals: $a < b/r \Rightarrow a \cdot r < b$

Informal description

For any non-negative real numbers $a, b, r \in \mathbb{R}_{\geq 0}$, if $a < b / r$, then $a \cdot r < b$.

NNReal.div_le_div_left_of_le theorem

{a b c : ℝ≥0} (c0 : c ≠ 0) (cb : c ≤ b) : a / b ≤ a / c

Full source

@[deprecated div_le_div_of_nonneg_left (since := "2024-11-12")]
theorem div_le_div_left_of_le {a b c : ℝ≥0} (c0 : c ≠ 0) (cb : c ≤ b) :
    a / b ≤ a / c :=
  div_le_div_of_nonneg_left (zero_le _) c0.bot_lt cb

Division Inequality for Non-Negative Reals: $\frac{a}{b} \leq \frac{a}{c}$ when $0 < c \leq b$

Informal description

For any non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0}$ with $c \neq 0$ and $c \leq b$, the inequality $\frac{a}{b} \leq \frac{a}{c}$ holds.

NNReal.div_le_div_left theorem

{a b c : ℝ≥0} (a0 : 0 < a) (b0 : 0 < b) (c0 : 0 < c) : a / b ≤ a / c ↔ c ≤ b

Full source

@[deprecated div_le_div_iff_of_pos_left (since := "2024-11-12")]
nonrec theorem div_le_div_left {a b c : ℝ≥0} (a0 : 0 < a) (b0 : 0 < b) (c0 : 0 < c) :
    a / b ≤ a / c ↔ c ≤ b :=
  div_le_div_iff_of_pos_left a0 b0 c0

Division Inequality for Positive Non-Negative Reals: $\frac{a}{b} \leq \frac{a}{c} \leftrightarrow c \leq b$ when $a, b, c > 0$

Informal description

For any positive non-negative real numbers $a, b, c > 0$ in $\mathbb{R}_{\geq 0}$, the inequality $\frac{a}{b} \leq \frac{a}{c}$ holds if and only if $c \leq b$.

NNReal.le_of_forall_lt_one_mul_le theorem

{x y : ℝ≥0} (h : ∀ a < 1, a * x ≤ y) : x ≤ y

Full source

theorem le_of_forall_lt_one_mul_le {x y : ℝ≥0} (h : ∀ a < 1, a * x ≤ y) : x ≤ y :=
  le_of_forall_lt_imp_le_of_dense fun a ha => by
    have hx : x ≠ 0 := pos_iff_ne_zero.1 (lt_of_le_of_lt (zero_le _) ha)
    have hx' : x⁻¹x⁻¹ ≠ 0 := by rwa [Ne, inv_eq_zero]
    have : a * x⁻¹ < 1 := by rwa [← lt_inv_iff_mul_lt hx', inv_inv]
    have : a * x⁻¹ * x ≤ y := h _ this
    rwa [mul_assoc, inv_mul_cancel₀ hx, mul_one] at this

Non-negative real number inequality via scaling by numbers less than one

Informal description

For any non-negative real numbers $x$ and $y$, if for every $a < 1$ the inequality $a \cdot x \leq y$ holds, then $x \leq y$.

NNReal.half_le_self theorem

(a : ℝ≥0) : a / 2 ≤ a

Full source

nonrec theorem half_le_self (a : ℝ≥0) : a / 2 ≤ a :=
  half_le_self bot_le

Non-negative real number halving inequality: $\frac{a}{2} \leq a$

Informal description

For any non-negative real number $a \in \mathbb{R}_{\geq 0}$, the inequality $\frac{a}{2} \leq a$ holds.

NNReal.half_lt_self theorem

{a : ℝ≥0} (h : a ≠ 0) : a / 2 < a

Full source

nonrec theorem half_lt_self {a : ℝ≥0} (h : a ≠ 0) : a / 2 < a :=
  half_lt_self h.bot_lt

Half of a Nonzero Non-Negative Real Number is Strictly Less Than Itself

Informal description

For any nonzero non-negative real number $a \in \mathbb{R}_{\geq 0}$, the inequality $a/2 < a$ holds.

NNReal.div_lt_one_of_lt theorem

{a b : ℝ≥0} (h : a < b) : a / b < 1

Full source

theorem div_lt_one_of_lt {a b : ℝ≥0} (h : a < b) : a / b < 1 := by
  rwa [div_lt_iff₀ h.bot_lt, one_mul]

Ratio of Non-negative Reals Less Than One When Numerator is Less Than Denominator

Informal description

For any non-negative real numbers $a$ and $b$ such that $a < b$, the ratio $a / b$ is strictly less than $1$.

Real.toNNReal_inv theorem

{x : ℝ} : Real.toNNReal x⁻¹ = (Real.toNNReal x)⁻¹

Full source

theorem _root_.Real.toNNReal_inv {x : ℝ} : Real.toNNReal x⁻¹ = (Real.toNNReal x)⁻¹ := by
  rcases le_total 0 x with hx | hx
  · nth_rw 1 [← Real.coe_toNNReal x hx]
    rw [← NNReal.coe_inv, Real.toNNReal_coe]
  · rw [toNNReal_eq_zero.mpr hx, inv_zero, toNNReal_eq_zero.mpr (inv_nonpos.mpr hx)]

Inverse Preservation in Non-negative Part: $\text{toNNReal}(x^{-1}) = (\text{toNNReal}(x))^{-1}$

Informal description

For any real number $x$, the non-negative part of its multiplicative inverse equals the multiplicative inverse of the non-negative part of $x$, i.e., $\text{toNNReal}(x^{-1}) = (\text{toNNReal}(x))^{-1}$.

Real.toNNReal_div theorem

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

Full source

theorem _root_.Real.toNNReal_div {x y : ℝ} (hx : 0 ≤ x) :
    Real.toNNReal (x / y) = Real.toNNReal x / Real.toNNReal y := by
  rw [div_eq_mul_inv, div_eq_mul_inv, ← Real.toNNReal_inv, ← Real.toNNReal_mul hx]

Multiplicativity of Non-negative Part for Ratios with Non-negative Numerator: $\text{toNNReal}(x/y) = \text{toNNReal}(x)/\text{toNNReal}(y)$

Informal description

For any real numbers $x$ and $y$ with $x \geq 0$, the non-negative part of the ratio $x/y$ equals the ratio of the non-negative parts of $x$ and $y$, i.e., \[ \text{toNNReal}\left(\frac{x}{y}\right) = \frac{\text{toNNReal}(x)}{\text{toNNReal}(y)}. \]

Real.toNNReal_div' theorem

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

Full source

theorem _root_.Real.toNNReal_div' {x y : ℝ} (hy : 0 ≤ y) :
    Real.toNNReal (x / y) = Real.toNNReal x / Real.toNNReal y := by
  rw [div_eq_inv_mul, div_eq_inv_mul, Real.toNNReal_mul (inv_nonneg.2 hy), Real.toNNReal_inv]

Multiplicativity of Non-negative Part for Quotient with Non-negative Denominator

Informal description

For any real numbers $x$ and $y$ with $y \geq 0$, the non-negative part of the quotient $x / y$ equals the quotient of the non-negative parts of $x$ and $y$, i.e., \[ \text{toNNReal}(x / y) = \text{toNNReal}(x) / \text{toNNReal}(y). \]

NNReal.inv_lt_one_iff theorem

{x : ℝ≥0} (hx : x ≠ 0) : x⁻¹ < 1 ↔ 1 < x

Full source

theorem inv_lt_one_iff {x : ℝ≥0} (hx : x ≠ 0) : x⁻¹x⁻¹ < 1 ↔ 1 < x := by
  rw [← one_div, div_lt_iff₀ hx.bot_lt, one_mul]

Inverse Inequality for Non-Negative Reals: $x^{-1} < 1 \leftrightarrow 1 < x$

Informal description

For any nonzero non-negative real number $x \in \mathbb{R}_{\geq 0}$, the inequality $x^{-1} < 1$ holds if and only if $1 < x$.

NNReal.inv_lt_inv theorem

{x y : ℝ≥0} (hx : x ≠ 0) (h : x < y) : y⁻¹ < x⁻¹

Full source

theorem inv_lt_inv {x y : ℝ≥0} (hx : x ≠ 0) (h : x < y) : y⁻¹ < x⁻¹ :=
  inv_strictAnti₀ hx.bot_lt h

Inverse Reverses Inequality for Non-Negative Real Numbers: $x < y \Rightarrow y^{-1} < x^{-1}$ when $x \neq 0$

Informal description

For any nonzero non-negative real numbers $x, y \in \mathbb{R}_{\geq 0}$ such that $x < y$, the inequality $y^{-1} < x^{-1}$ holds.

NNReal.exists_nat_pos_inv_lt theorem

{b : ℝ≥0} (hb : 0 < b) : ∃ (n : ℕ), 0 < n ∧ (n : ℝ≥0)⁻¹ < b

Full source

lemma exists_nat_pos_inv_lt {b : ℝ≥0} (hb : 0 < b) :
    ∃ (n : ℕ), 0 < n ∧ (n : ℝ≥0)⁻¹ < b :=
  b.toReal.exists_nat_pos_inv_lt hb

Existence of Natural Number with Small Reciprocal in Non-Negative Reals

Informal description

For any positive non-negative real number $b > 0$, there exists a positive natural number $n$ such that the reciprocal of $n$ (as a non-negative real number) is less than $b$, i.e., $n^{-1} < b$.

NNReal.abs_eq theorem

(x : ℝ≥0) : |(x : ℝ)| = x

Full source

@[simp]
theorem abs_eq (x : ℝ≥0) : |(x : ℝ)| = x :=
  abs_of_nonneg x.property

Absolute Value Identity for Non-Negative Real Numbers: $|x| = x$

Informal description

For any non-negative real number $x \in \mathbb{R}_{\geq 0}$, the absolute value of $x$ (as an element of $\mathbb{R}$) equals $x$ itself, i.e., $|x| = x$.

NNReal.le_toNNReal_of_coe_le theorem

{x : ℝ≥0} {y : ℝ} (h : ↑x ≤ y) : x ≤ y.toNNReal

Full source

theorem le_toNNReal_of_coe_le {x : ℝ≥0} {y : ℝ} (h : ↑x ≤ y) : x ≤ y.toNNReal :=
  (le_toNNReal_iff_coe_le <| x.2.trans h).2 h

Inequality Preservation from Real to Non-Negative Real Numbers: $x \leq \text{toNNReal}(y)$ given $\uparrow x \leq y$

Informal description

For any non-negative real number $x \in \mathbb{R}_{\geq 0}$ and any real number $y \in \mathbb{R}$, if the underlying real value of $x$ satisfies $\uparrow x \leq y$, then $x$ is less than or equal to the non-negative part of $y$, i.e., $x \leq \text{toNNReal}(y)$.

NNReal.sSup_of_not_bddAbove theorem

{s : Set ℝ≥0} (hs : ¬BddAbove s) : SupSet.sSup s = 0

Full source

nonrec theorem sSup_of_not_bddAbove {s : Set ℝ≥0} (hs : ¬BddAbove s) : SupSet.sSup s = 0 := by
  rw [← bddAbove_coe] at hs
  rw [← coe_inj, coe_sSup, NNReal.coe_zero]
  exact sSup_of_not_bddAbove hs

Supremum of Unbounded Above Set in Non-Negative Reals is Zero

Informal description

For any subset $s$ of the non-negative real numbers $\mathbb{R}_{\geq 0}$ that is not bounded above, the supremum of $s$ is equal to $0$.

NNReal.iSup_of_not_bddAbove theorem

(hf : ¬BddAbove (range f)) : ⨆ i, f i = 0

Full source

theorem iSup_of_not_bddAbove (hf : ¬BddAbove (range f)) : ⨆ i, f i = 0 :=
  sSup_of_not_bddAbove hf

Supremum of Unbounded Above Non-Negative Real Function is Zero

Informal description

For any function $f : \iota \to \mathbb{R}_{\geq 0}$ whose range is not bounded above, the supremum of $f$ over its domain is equal to $0$, i.e., $\bigsqcup_{i} f(i) = 0$.

NNReal.iSup_empty theorem

[IsEmpty ι] (f : ι → ℝ≥0) : ⨆ i, f i = 0

Full source

theorem iSup_empty [IsEmpty ι] (f : ι → ℝ≥0) : ⨆ i, f i = 0 := ciSup_of_empty f

Supremum over Empty Index Set is Zero in Non-Negative Reals

Informal description

For any empty index type $\iota$ and any function $f : \iota \to \mathbb{R}_{\geq 0}$, the supremum of $f$ over $\iota$ is equal to $0$, i.e., $\bigsqcup_{i \in \iota} f(i) = 0$.

NNReal.iInf_empty theorem

[IsEmpty ι] (f : ι → ℝ≥0) : ⨅ i, f i = 0

Full source

theorem iInf_empty [IsEmpty ι] (f : ι → ℝ≥0) : ⨅ i, f i = 0 := by
  rw [_root_.iInf_of_isEmpty, sInf_empty]

Infimum over Empty Index Set is Zero in Non-Negative Reals

Informal description

For any empty index type $\iota$ and any function $f : \iota \to \mathbb{R}_{\geq 0}$, the infimum of $f$ over $\iota$ is equal to $0$, i.e., $\bigsqcap_{i \in \iota} f(i) = 0$.

NNReal.iSup_eq_zero theorem

(hf : BddAbove (range f)) : ⨆ i, f i = 0 ↔ ∀ i, f i = 0

Full source

@[simp] lemma iSup_eq_zero (hf : BddAbove (range f)) : ⨆ i, f i⨆ i, f i = 0 ↔ ∀ i, f i = 0 := by
  cases isEmpty_or_nonempty ι
  · simp
  · simp [← bot_eq_zero', ← le_bot_iff, ciSup_le_iff hf]

Characterization of Zero Supremum for Bounded Non-Negative Real-Valued Functions: $\bigsqcup_i f(i) = 0 \leftrightarrow \forall i, f(i) = 0$

Informal description

Let $f : \iota \to \mathbb{R}_{\geq 0}$ be a function with bounded range. Then the supremum of $f$ equals $0$ if and only if $f(i) = 0$ for all $i \in \iota$. In other words, $\bigsqcup_{i} f(i) = 0 \leftrightarrow \forall i, f(i) = 0$.

NNReal.iInf_const_zero theorem

{α : Sort*} : ⨅ _ : α, (0 : ℝ≥0) = 0

Full source

@[simp]
theorem iInf_const_zero {α : Sort*} : ⨅ _ : α, (0 : ℝ≥0) = 0 := by
  rw [← coe_inj, coe_iInf]
  exact Real.iInf_const_zero

Infimum of Constant Zero Function in Non-Negative Reals: $\bigsqcap_{i \in \alpha} 0 = 0$

Informal description

For any index type $\alpha$, the infimum of the constant zero function over $\alpha$ is equal to $0$ in the non-negative real numbers $\mathbb{R}_{\geq 0}$, i.e., $\bigsqcap_{i \in \alpha} 0 = 0$.

Set.OrdConnected.preimage_coe_nnreal_real theorem

(h : s.OrdConnected) : ((↑) ⁻¹' s : Set ℝ≥0).OrdConnected

Full source

theorem preimage_coe_nnreal_real (h : s.OrdConnected) : ((↑)(↑) ⁻¹' s : Set ℝ≥0).OrdConnected :=
  h.preimage_mono NNReal.coe_mono

Order-Connectedness of Preimage under Non-Negative Real Inclusion

Informal description

Let $s$ be an order-connected subset of $\mathbb{R}$. Then the preimage of $s$ under the canonical inclusion map from non-negative real numbers $\mathbb{R}_{\geq 0}$ to $\mathbb{R}$ is also order-connected in $\mathbb{R}_{\geq 0}$.

Set.OrdConnected.image_coe_nnreal_real theorem

(h : t.OrdConnected) : ((↑) '' t : Set ℝ).OrdConnected

Full source

theorem image_coe_nnreal_real (h : t.OrdConnected) : ((↑)(↑) '' t : Set ℝ).OrdConnected :=
  ⟨forall_mem_image.2 fun x hx =>
      forall_mem_image.2 fun _y hy z hz => ⟨⟨z, x.2.trans hz.1⟩, h.out hx hy hz, rfl⟩⟩

Order-Connectedness Preservation under Inclusion from Non-Negative Reals to Reals

Informal description

Let $t$ be an order-connected subset of the non-negative real numbers $\mathbb{R}_{\geq 0}$. Then the image of $t$ under the canonical inclusion map $\mathbb{R}_{\geq 0} \to \mathbb{R}$ is also order-connected in $\mathbb{R}$.

Set.OrdConnected.image_real_toNNReal theorem

(h : s.OrdConnected) : (Real.toNNReal '' s).OrdConnected

Full source

theorem image_real_toNNReal (h : s.OrdConnected) : (Real.toNNRealReal.toNNReal '' s).OrdConnected := by
  refine ⟨forall_mem_image.2 fun x hx => forall_mem_image.2 fun y hy z hz => ?_⟩
  rcases le_total y 0 with hy₀ | hy₀
  · rw [mem_Icc, Real.toNNReal_of_nonpos hy₀, nonpos_iff_eq_zero] at hz
    exact ⟨y, hy, (toNNReal_of_nonpos hy₀).trans hz.2.symm⟩
  · lift y to ℝ≥0 using hy₀
    rw [toNNReal_coe] at hz
    exact ⟨z, h.out hx hy ⟨toNNReal_le_iff_le_coe.1 hz.1, hz.2⟩, toNNReal_coe⟩

Order-Connectedness Preservation under Non-Negative Part Function

Informal description

Let $s$ be an order-connected subset of the real numbers $\mathbb{R}$. Then the image of $s$ under the function $\operatorname{toNNReal} : \mathbb{R} \to \mathbb{R}_{\geq 0}$ (defined by $\operatorname{toNNReal}(x) = \max(x, 0)$) is order-connected in $\mathbb{R}_{\geq 0}$.

Set.OrdConnected.preimage_real_toNNReal theorem

(h : t.OrdConnected) : (Real.toNNReal ⁻¹' t).OrdConnected

Full source

theorem preimage_real_toNNReal (h : t.OrdConnected) : (Real.toNNRealReal.toNNReal ⁻¹' t).OrdConnected :=
  h.preimage_mono Real.toNNReal_mono

Order-Connectedness of Preimage under Non-Negative Part Function

Informal description

Let $t$ be an order-connected subset of the non-negative real numbers $\mathbb{R}_{\geq 0}$. Then the preimage of $t$ under the function $\operatorname{toNNReal} : \mathbb{R} \to \mathbb{R}_{\geq 0}$ (defined by $\operatorname{toNNReal}(x) = \max(x, 0)$) is order-connected in $\mathbb{R}$.

Real.nnabs definition

: ℝ →*₀ ℝ≥0

Full source

/-- The absolute value on `ℝ` as a map to `ℝ≥0`. -/
-- Porting note (kmill): `pp_nodot` has no affect here
-- unless RFC https://github.com/leanprover/lean4/issues/6178 leads to dot notation pp for CoeFun
@[pp_nodot]
def nnabs : ℝℝ →*₀ ℝ≥0 where
  toFun x := ⟨|x|, abs_nonneg x⟩
  map_zero' := by ext; simp
  map_one' := by ext; simp
  map_mul' x y := by ext; simp [abs_mul]

Absolute value as a non-negative real number

Informal description

The function maps a real number $ x $ to its absolute value $ |x| $ as a non-negative real number. It preserves multiplication, zero, and one.

Real.coe_nnabs theorem

(x : ℝ) : (nnabs x : ℝ) = |x|

Full source

@[norm_cast, simp]
theorem coe_nnabs (x : ℝ) : (nnabs x : ℝ) = |x| :=
  rfl

Equality of Non-Negative Absolute Value and Absolute Value on Reals

Informal description

For any real number $x$, the underlying real number of its non-negative absolute value $\operatorname{nnabs}(x)$ is equal to the absolute value of $x$, i.e., $\operatorname{nnabs}(x) = |x|$.

Real.nnabs_of_nonneg theorem

{x : ℝ} (h : 0 ≤ x) : nnabs x = toNNReal x

Full source

@[simp]
theorem nnabs_of_nonneg {x : ℝ} (h : 0 ≤ x) : nnabs x = toNNReal x := by
  ext
  rw [coe_toNNReal x h, coe_nnabs, abs_of_nonneg h]

Non-negative absolute value equals non-negative part for non-negative reals

Informal description

For any real number $x$ such that $0 \leq x$, the non-negative absolute value of $x$ is equal to the non-negative part of $x$, i.e., $\operatorname{nnabs}(x) = \operatorname{toNNReal}(x)$.

Real.nnabs_coe theorem

(x : ℝ≥0) : nnabs x = x

Full source

theorem nnabs_coe (x : ℝ≥0) : nnabs x = x := by simp

Identity for Non-Negative Absolute Value on Non-Negative Reals: $\operatorname{nnabs}(x) = x$

Informal description

For any non-negative real number $x \in \mathbb{R}_{\geq 0}$, the non-negative absolute value of $x$ is equal to $x$ itself, i.e., $\operatorname{nnabs}(x) = x$.

Real.coe_toNNReal_le theorem

(x : ℝ) : (toNNReal x : ℝ) ≤ |x|

Full source

theorem coe_toNNReal_le (x : ℝ) : (toNNReal x : ℝ) ≤ |x| :=
  max_le (le_abs_self _) (abs_nonneg _)

Non-negative part is bounded by absolute value: $\text{toNNReal}(x) \leq |x|$

Informal description

For any real number $x$, the image of $x$ under the `toNNReal` function (which takes the maximum of $x$ and $0$) is less than or equal to the absolute value of $x$, i.e., $\text{toNNReal}(x) \leq |x|$.

Real.toNNReal_abs theorem

(x : ℝ) : |x|.toNNReal = nnabs x

Full source

@[simp] lemma toNNReal_abs (x : ℝ) : |x|.toNNReal = nnabs x := NNReal.coe_injective <| by simp

Equality of Non-negative Part and Absolute Value: $\text{toNNReal}(|x|) = \text{nnabs}(x)$

Informal description

For any real number $x$, the non-negative part of the absolute value of $x$ is equal to the non-negative absolute value of $x$, i.e., $\text{toNNReal}(|x|) = \text{nnabs}(x)$.

Real.cast_natAbs_eq_nnabs_cast theorem

(n : ℤ) : (n.natAbs : ℝ≥0) = nnabs n

Full source

theorem cast_natAbs_eq_nnabs_cast (n : ℤ) : (n.natAbs : ℝ≥0) = nnabs n := by
  ext
  rw [NNReal.coe_natCast, Int.cast_natAbs, Real.coe_nnabs, Int.cast_abs]

Equality of Natural Absolute Value Cast and Non-Negative Absolute Value: $(|n|_{\mathbb{N}} : \mathbb{R}_{\geq 0}) = \operatorname{nnabs}(n)$

Informal description

For any integer $n$, the non-negative real number obtained by casting the natural absolute value of $n$ is equal to the non-negative absolute value of $n$ as a real number, i.e., $(|n|_{\mathbb{N}} : \mathbb{R}_{\geq 0}) = \operatorname{nnabs}(n)$.

Real.nnreal_dichotomy theorem

(r : ℝ) : ∃ x : ℝ≥0, r = x ∨ r = -x

Full source

/-- Every real number nonnegative or nonpositive, phrased using `ℝ≥0`. -/
lemma nnreal_dichotomy (r : ℝ) : ∃ x : ℝ≥0, r = x ∨ r = -x := by
  obtain (hr | hr) : 0 ≤ r ∨ 0 ≤ -r := by simpa using le_total ..
  all_goals
    rw [← neg_neg r]
    lift (_ : ℝ) to ℝ≥0 using hr with r
    aesop

Dichotomy for Real Numbers: $r = x$ or $r = -x$ for some $x \geq 0$

Informal description

For every real number $r$, there exists a non-negative real number $x$ such that either $r = x$ or $r = -x$.

Real.nnreal_trichotomy theorem

(r : ℝ) : r = 0 ∨ ∃ x : ℝ≥0, 0 < x ∧ (r = x ∨ r = -x)

Full source

/-- Every real number is either zero, positive or negative, phrased using `ℝ≥0`. -/
lemma nnreal_trichotomy (r : ℝ) : r = 0 ∨ ∃ x : ℝ≥0, 0 < x ∧ (r = x ∨ r = -x) := by
  obtain ⟨x, hx⟩ := nnreal_dichotomy r
  rw [or_iff_not_imp_left]
  aesop (add simp pos_iff_ne_zero)

Trichotomy for Real Numbers: $r = 0$ or $r = x$ or $r = -x$ for some $x > 0$

Informal description

For every real number $r$, either $r = 0$ or there exists a positive non-negative real number $x$ (i.e., $x \in \mathbb{R}_{\geq 0}$ with $0 < x$) such that $r = x$ or $r = -x$.

Real.nnreal_induction_on theorem

 {motive : ℝ → Prop} (nonneg : ∀ x : ℝ≥0, motive x) (nonpos : ∀ x : ℝ≥0, motive x → motive (-x)) (r : ℝ) : motive r

Full source

/-- 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 : ℝ)`. -/
@[elab_as_elim]
lemma nnreal_induction_on {motive : ℝ → Prop} (nonneg : ∀ x : ℝ≥0, motive x)
    (nonpos : ∀ x : ℝ≥0, motive x → motive (-x)) (r : ℝ) : motive r := by
  obtain ⟨r, (rfl | rfl)⟩ := r.nnreal_dichotomy
  all_goals simp_all

Induction Principle for Real Numbers via Non-negative Case and Negation

Informal description

Let $motive : \mathbb{R} \to \text{Prop}$ be a property of real numbers. If: 1. $motive(x)$ holds for all non-negative real numbers $x \in \mathbb{R}_{\geq 0}$, and 2. For any $x \in \mathbb{R}_{\geq 0}$, if $motive(x)$ holds then $motive(-x)$ also holds, then $motive(r)$ holds for every real number $r \in \mathbb{R}$.

Real.nnreal_induction_on' theorem

 {motive : ℝ → Prop} (zero : motive 0) (pos : ∀ x : ℝ≥0, 0 < x → motive x)
  (neg : ∀ x : ℝ≥0, 0 < x → motive x → motive (-x)) (r : ℝ) : motive r

Full source

/-- A version of `nnreal_induction_on` which splits into three cases (zero, positive and negative)
instead of two. -/
@[elab_as_elim]
lemma nnreal_induction_on' {motive : ℝ → Prop} (zero : motive 0) (pos : ∀ x : ℝ≥0, 0 < x → motive x)
    (neg : ∀ x : ℝ≥0, 0 < x → motive x → motive (-x)) (r : ℝ) : motive r := by
  obtain rfl | ⟨r, hr, (rfl | rfl)⟩ := r.nnreal_trichotomy
  all_goals simp_all

Three-case Induction Principle for Real Numbers via Zero, Positive, and Negative Cases

Informal description

Let $motive : \mathbb{R} \to \text{Prop}$ be a property of real numbers. If: 1. $motive(0)$ holds, 2. For any positive non-negative real number $x \in \mathbb{R}_{\geq 0}$ (i.e., $0 < x$), $motive(x)$ holds, and 3. For any positive non-negative real number $x \in \mathbb{R}_{\geq 0}$, if $motive(x)$ holds then $motive(-x)$ also holds, then $motive(r)$ holds for every real number $r \in \mathbb{R}$.

NNReal.exists_lt_of_strictMono theorem

 [h : Nontrivial Γ₀ˣ] {f : Γ₀ →*₀ ℝ≥0} (hf : StrictMono f) {r : ℝ≥0} (hr : 0 < r) : ∃ d : Γ₀ˣ, f d < r

Full source

/-- If `Γ₀ˣ` is nontrivial and `f : Γ₀ →*₀ ℝ≥0` is strictly monotone, then for any positive
  `r : ℝ≥0`, there exists `d : Γ₀ˣ` with `f d < r`. -/
theorem NNReal.exists_lt_of_strictMono [h : Nontrivial Γ₀ˣ] {f : Γ₀ →*₀ ℝ≥0} (hf : StrictMono f)
    {r : ℝ≥0} (hr : 0 < r) : ∃ d : Γ₀ˣ, f d < r := by
  obtain ⟨g, hg1⟩ := (nontrivial_iff_exists_ne (1 : Γ₀ˣ)).mp h
  set u : Γ₀ˣ := if g < 1 then g else g⁻¹ with hu
  have hfu : f u < 1 := by
    rw [hu]
    split_ifs with hu1
    · rw [← map_one f]; exact hf hu1
    · have hfg0 : f g ≠ 0 :=
        fun h0 ↦ (Units.ne_zero g) ((map_eq_zero f).mp h0)
      have hg1' : 1 < g := lt_of_le_of_ne (not_lt.mp hu1) hg1.symm
      rw [Units.val_inv_eq_inv_val, map_inv₀, inv_lt_one_iff hfg0, ← map_one f]
      exact hf hg1'
  obtain ⟨n, hn⟩ := exists_pow_lt_of_lt_one hr hfu
  use u ^ n
  rwa [Units.val_pow_eq_pow_val, map_pow]

Existence of Unit with Small Image under Strictly Monotone Homomorphism in Ordered Group with Zero

Informal description

Let $\Gamma_0$ be a linearly ordered commutative group with zero, and let $\Gamma_0^\times$ be its group of units. If $\Gamma_0^\times$ is nontrivial and $f : \Gamma_0 \to \mathbb{R}_{\geq 0}$ is a strictly monotone monoid homomorphism with zero, then for any positive real number $r \in \mathbb{R}_{\geq 0}$ with $r > 0$, there exists a unit $d \in \Gamma_0^\times$ such that $f(d) < r$.

Real.exists_lt_of_strictMono theorem

 [h : Nontrivial Γ₀ˣ] {f : Γ₀ →*₀ ℝ≥0} (hf : StrictMono f) {r : ℝ} (hr : 0 < r) : ∃ d : Γ₀ˣ, (f d : ℝ) < r

Full source

/-- If `Γ₀ˣ` is nontrivial and `f : Γ₀ →*₀ ℝ≥0` is strictly monotone, then for any positive
  real `r`, there exists `d : Γ₀ˣ` with `f d < r`. -/
theorem Real.exists_lt_of_strictMono [h : Nontrivial Γ₀ˣ] {f : Γ₀ →*₀ ℝ≥0} (hf : StrictMono f)
    {r : ℝ} (hr : 0 < r) : ∃ d : Γ₀ˣ, (f d : ℝ) < r := by
  set s : NNReal := ⟨r, le_of_lt hr⟩
  have hs : 0 < s := hr
  exact NNReal.exists_lt_of_strictMono hf hs

Existence of Unit with Small Image under Strictly Monotone Homomorphism from Ordered Group to Non-negative Reals

Informal description

Let $\Gamma_0$ be a linearly ordered commutative group with zero, and let $\Gamma_0^\times$ be its group of units. If $\Gamma_0^\times$ is nontrivial and $f : \Gamma_0 \to \mathbb{R}_{\geq 0}$ is a strictly monotone monoid homomorphism with zero, then for any positive real number $r > 0$, there exists a unit $d \in \Gamma_0^\times$ such that the image of $d$ under $f$ (considered as a real number) satisfies $f(d) < r$.

instReprNNReal instance

: Repr ℝ≥0

Full source

/-- While not very useful, this instance uses the same representation as `Real.instRepr`. -/
unsafe instance : Repr ℝ≥0 where
  reprPrec r _ := f!"({repr r.val}).toNNReal"

String Representation of Non-Negative Real Numbers

Informal description

The non-negative real numbers $\mathbb{R}_{\geq 0}$ have a canonical string representation inherited from the real numbers.

Mathlib.Meta.Positivity.evalNNRealtoReal definition

: PositivityExt

Full source

/-- Extension for the `positivity` tactic: cast from `ℝ≥0` to `ℝ`. -/
@[positivity NNReal.toReal _]
def evalNNRealtoReal : PositivityExt where eval {u α} _zα _pα e := do
  match u, α, e with
  | 0, ~q(ℝ), ~q(NNReal.toReal $a) =>
    let ra ← core q(inferInstance) q(inferInstance) a
    assertInstancesCommute
    match ra with
    | .positive pa => pure (.positive q(nnreal_coe_pos $pa))
    | _ => pure (.nonnegative q(NNReal.coe_nonneg $a))
  | _, _, _ => throwError "not NNReal.toReal"

Positivity extension for non-negative real to real conversion

Informal description

The positivity extension for the function `NNReal.toReal`, which converts a non-negative real number to a real number. For an expression `NNReal.toReal a`, this extension determines its positivity properties based on the positivity of `a`: - If `a` is positive, then `NNReal.toReal a` is positive. - Otherwise, `NNReal.toReal a` is non-negative.

Notations