# Maps between real and extended non-negative real numbers #

This file focuses on the functions `ENNReal.toReal : ℝ≥0∞ → ℝ` and `ENNReal.ofReal : ℝ → ℝ≥0∞` which were defined in `Data.ENNReal.Basic`. It collects all the basic results of the interactions between these functions and the algebraic and lattice operations, although a few may appear in earlier files.

This file provides a `positivity` extension for `ENNReal.ofReal`.

## Main statements #

- `trichotomy (p : ℝ≥0∞) : p = 0 ∨ p = ∞ ∨ 0 < p.toReal`: often used for `WithLp` and `lp`
- `dichotomy (p : ℝ≥0∞) [Fact (1 ≤ p)] : p = ∞ ∨ 1 ≤ p.toReal`: often used for `WithLp` and `lp`
- `toNNReal_iInf` through `toReal_sSup`: these declarations allow for easy conversions between indexed or set infima and suprema in `ℝ`, `ℝ≥0` and `ℝ≥0∞`. This is especially useful because `ℝ≥0∞` is a complete lattice.

source
theorem ENNReal.toReal_add {a b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :
(a + b).toReal = a.toReal + b.toReal
source
theorem ENNReal.toReal_add_le {a b : ENNReal} :
(a + b).toReal ≤ a.toReal + b.toReal
source
theorem ENNReal.ofReal_add {p q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) :
ENNReal.ofReal (p + q) = ENNReal.ofReal p + ENNReal.ofReal q
source
theorem ENNReal.ofReal_add_le {p q : ℝ} :
ENNReal.ofReal (p + q) ≤ ENNReal.ofReal p + ENNReal.ofReal q
source
@[simp]
theorem ENNReal.toReal_le_toReal {a b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :
a.toReal ≤ b.toReal ↔ a ≤ b
source
theorem ENNReal.toReal_mono {a b : ENNReal} (hb : b ≠ ⊤) (h : a ≤ b) :
a.toReal ≤ b.toReal
source
theorem ENNReal.toReal_mono' {a b : ENNReal} (h : a ≤ b) (ht : b = ⊤ → a = ⊤) :
a.toReal ≤ b.toReal
source
@[simp]
theorem ENNReal.toReal_lt_toReal {a b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :
a.toReal < b.toReal ↔ a < b
source
theorem ENNReal.toReal_strict_mono {a b : ENNReal} (hb : b ≠ ⊤) (h : a < b) :
a.toReal < b.toReal
source
theorem ENNReal.toNNReal_mono {a b : ENNReal} (hb : b ≠ ⊤) (h : a ≤ b) :
a.toNNReal ≤ b.toNNReal
source
theorem ENNReal.le_toNNReal_of_coe_le {a : ENNReal} {p : NNReal} (h : ↑p ≤ a) (ha : a ≠ ⊤) :
p ≤ a.toNNReal
source
@[simp]
theorem ENNReal.toNNReal_le_toNNReal {a b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :
a.toNNReal ≤ b.toNNReal ↔ a ≤ b
source
theorem ENNReal.toNNReal_strict_mono {a b : ENNReal} (hb : b ≠ ⊤) (h : a < b) :
a.toNNReal < b.toNNReal
source
@[simp]
theorem ENNReal.toNNReal_lt_toNNReal {a b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :
a.toNNReal < b.toNNReal ↔ a < b
source
theorem ENNReal.toNNReal_lt_of_lt_coe {a : ENNReal} {p : NNReal} (h : a < ↑p) :
a.toNNReal < p
source
theorem ENNReal.toReal_max {a b : ENNReal} (hr : a ≠ ⊤) (hp : b ≠ ⊤) :
(max a b).toReal = max a.toReal b.toReal
source
theorem ENNReal.toReal_min {a b : ENNReal} (hr : a ≠ ⊤) (hp : b ≠ ⊤) :
(min a b).toReal = min a.toReal b.toReal
source
theorem ENNReal.toReal_sup {a b : ENNReal} :
a ≠ ⊤ → b ≠ ⊤ → (max a b).toReal = max a.toReal b.toReal
source
theorem ENNReal.toReal_inf {a b : ENNReal} :
a ≠ ⊤ → b ≠ ⊤ → (min a b).toReal = min a.toReal b.toReal
source
theorem ENNReal.toNNReal_pos_iff {a : ENNReal} :
0 < a.toNNReal ↔ 0 < a ∧ a < ⊤
source
theorem ENNReal.toNNReal_pos {a : ENNReal} (ha₀ : a ≠ 0) (ha_top : a ≠ ⊤) :
0 < a.toNNReal
source
theorem ENNReal.toReal_pos_iff {a : ENNReal} :
0 < a.toReal ↔ 0 < a ∧ a < ⊤
source
theorem ENNReal.toReal_pos {a : ENNReal} (ha₀ : a ≠ 0) (ha_top : a ≠ ⊤) :
0 < a.toReal
source
theorem ENNReal.ofReal_le_ofReal {p q : ℝ} (h : p ≤ q) :
ENNReal.ofReal p ≤ ENNReal.ofReal q
source
theorem ENNReal.ofReal_mono :
Monotone ENNReal.ofReal
source
theorem ENNReal.ofReal_le_of_le_toReal {a : ℝ} {b : ENNReal} (h : a ≤ b.toReal) :
ENNReal.ofReal a ≤ b
source
@[simp]
theorem ENNReal.ofReal_le_ofReal_iff {p q : ℝ} (h : 0 ≤ q) :
ENNReal.ofReal p ≤ ENNReal.ofReal q ↔ p ≤ q
source
theorem ENNReal.ofReal_le_ofReal_iff' {p q : ℝ} :
ENNReal.ofReal p ≤ ENNReal.ofReal q ↔ p ≤ q ∨ p ≤ 0
source
@[simp]
theorem ENNReal.ofReal_le_coe {a : ℝ} {b : NNReal} :
ENNReal.ofReal a ≤ ↑b ↔ a ≤ ↑b
source
theorem ENNReal.ofReal_lt_ofReal_iff' {p q : ℝ} :
ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q ∧ 0 < q
source
@[simp]
theorem ENNReal.ofReal_eq_ofReal_iff {p q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) :
ENNReal.ofReal p = ENNReal.ofReal q ↔ p = q
source
@[simp]
theorem ENNReal.ofReal_lt_ofReal_iff {p q : ℝ} (h : 0 < q) :
ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q
source
theorem ENNReal.ofReal_lt_ofReal_iff_of_nonneg {p q : ℝ} (hp : 0 ≤ p) :
ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q
source
@[simp]
theorem ENNReal.ofReal_pos {p : ℝ} :
0 < ENNReal.ofReal p ↔ 0 < p
source
@[simp]
theorem ENNReal.ofReal_eq_zero {p : ℝ} :
ENNReal.ofReal p = 0 ↔ p ≤ 0
source
@[simp]
theorem ENNReal.ofReal_min (x y : ℝ) :
ENNReal.ofReal (min x y) = min (ENNReal.ofReal x) (ENNReal.ofReal y)
source
@[simp]
theorem ENNReal.ofReal_max (x y : ℝ) :
ENNReal.ofReal (max x y) = max (ENNReal.ofReal x) (ENNReal.ofReal y)
source
theorem ENNReal.ofReal_ne_zero_iff {r : ℝ} :
ENNReal.ofReal r ≠ 0 ↔ 0 < r
source
@[simp]
theorem ENNReal.zero_eq_ofReal {p : ℝ} :
0 = ENNReal.ofReal p ↔ p ≤ 0
source
theorem ENNReal.ofReal_of_nonpos {p : ℝ} :
p ≤ 0 → ENNReal.ofReal p = 0

Alias of the reverse direction of `ENNReal.ofReal_eq_zero`.

source
@[simp]
theorem ENNReal.ofReal_lt_natCast {p : ℝ} {n : ℕ} (hn : n ≠ 0) :
ENNReal.ofReal p < ↑n ↔ p < ↑n
source
@[simp]
theorem ENNReal.ofReal_lt_one {p : ℝ} :
ENNReal.ofReal p < 1 ↔ p < 1
source
@[simp]
theorem ENNReal.ofReal_lt_ofNat {p : ℝ} {n : ℕ} [n.AtLeastTwo] :
ENNReal.ofReal p < OfNat.ofNat n ↔ p < OfNat.ofNat n
source
@[simp]
theorem ENNReal.natCast_le_ofReal {n : ℕ} {p : ℝ} (hn : n ≠ 0) :
↑n ≤ ENNReal.ofReal p ↔ ↑n ≤ p
source
@[simp]
theorem ENNReal.one_le_ofReal {p : ℝ} :
1 ≤ ENNReal.ofReal p ↔ 1 ≤ p
source
@[simp]
theorem ENNReal.ofNat_le_ofReal {n : ℕ} [n.AtLeastTwo] {p : ℝ} :
OfNat.ofNat n ≤ ENNReal.ofReal p ↔ OfNat.ofNat n ≤ p
source
@[simp]
theorem ENNReal.ofReal_le_natCast {r : ℝ} {n : ℕ} :
ENNReal.ofReal r ≤ ↑n ↔ r ≤ ↑n
source
@[simp]
theorem ENNReal.ofReal_le_one {r : ℝ} :
ENNReal.ofReal r ≤ 1 ↔ r ≤ 1
source
@[simp]
theorem ENNReal.ofReal_le_ofNat {r : ℝ} {n : ℕ} [n.AtLeastTwo] :
ENNReal.ofReal r ≤ OfNat.ofNat n ↔ r ≤ OfNat.ofNat n
source
@[simp]
theorem ENNReal.natCast_lt_ofReal {n : ℕ} {r : ℝ} :
↑n < ENNReal.ofReal r ↔ ↑n < r
source
@[simp]
theorem ENNReal.one_lt_ofReal {r : ℝ} :
1 < ENNReal.ofReal r ↔ 1 < r
source
@[simp]
theorem ENNReal.ofNat_lt_ofReal {n : ℕ} [n.AtLeastTwo] {r : ℝ} :
OfNat.ofNat n < ENNReal.ofReal r ↔ OfNat.ofNat n < r
source
@[simp]
theorem ENNReal.ofReal_eq_natCast {r : ℝ} {n : ℕ} (h : n ≠ 0) :
ENNReal.ofReal r = ↑n ↔ r = ↑n
source
@[simp]
theorem ENNReal.ofReal_eq_one {r : ℝ} :
ENNReal.ofReal r = 1 ↔ r = 1
source
@[simp]
theorem ENNReal.ofReal_eq_ofNat {r : ℝ} {n : ℕ} [n.AtLeastTwo] :
ENNReal.ofReal r = OfNat.ofNat n ↔ r = OfNat.ofNat n
source
theorem ENNReal.ofReal_le_iff_le_toReal {a : ℝ} {b : ENNReal} (hb : b ≠ ⊤) :
ENNReal.ofReal a ≤ b ↔ a ≤ b.toReal
source
theorem ENNReal.ofReal_lt_iff_lt_toReal {a : ℝ} {b : ENNReal} (ha : 0 ≤ a) (hb : b ≠ ⊤) :
ENNReal.ofReal a < b ↔ a < b.toReal
source
theorem ENNReal.ofReal_lt_coe_iff {a : ℝ} {b : NNReal} (ha : 0 ≤ a) :
ENNReal.ofReal a < ↑b ↔ a < ↑b
source
theorem ENNReal.le_ofReal_iff_toReal_le {a : ENNReal} {b : ℝ} (ha : a ≠ ⊤) (hb : 0 ≤ b) :
a ≤ ENNReal.ofReal b ↔ a.toReal ≤ b
source
theorem ENNReal.toReal_le_of_le_ofReal {a : ENNReal} {b : ℝ} (hb : 0 ≤ b) (h : a ≤ ENNReal.ofReal b) :
a.toReal ≤ b
source
theorem ENNReal.lt_ofReal_iff_toReal_lt {a : ENNReal} {b : ℝ} (ha : a ≠ ⊤) :
a < ENNReal.ofReal b ↔ a.toReal < b
source
theorem ENNReal.toReal_lt_of_lt_ofReal {a : ENNReal} {b : ℝ} (h : a < ENNReal.ofReal b) :
a.toReal < b
source
@[simp]
theorem ENNReal.ofReal_mul {p q : ℝ} (hp : 0 ≤ p) :
ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q
source
theorem ENNReal.ofReal_mul' {p q : ℝ} (hq : 0 ≤ q) :
ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q
source
@[simp]
theorem ENNReal.ofReal_pow {p : ℝ} (hp : 0 ≤ p) (n : ℕ) :
ENNReal.ofReal (p ^ n) = ENNReal.ofReal p ^ n
source
theorem ENNReal.ofReal_nsmul {x : ℝ} {n : ℕ} :
ENNReal.ofReal (n • x) = n • ENNReal.ofReal x
source
@[simp]
theorem ENNReal.toNNReal_mul {a b : ENNReal} :
(a * b).toNNReal = a.toNNReal * b.toNNReal
source
theorem ENNReal.toNNReal_mul_top (a : ENNReal) :
(a * ⊤).toNNReal = 0
source
theorem ENNReal.toNNReal_top_mul (a : ENNReal) :
(⊤ * a).toNNReal = 0
source
def ENNReal.toNNRealHom :
ENNReal →*₀ NNReal

`ENNReal.toNNReal` as a `MonoidHom`.

Equations

- ENNReal.toNNRealHom = { toFun := ENNReal.toNNReal, map_zero' := ENNReal.toNNReal_zero, map_one' := ENNReal.toNNRealHom._proof_1, map_mul' := ⋯ }

Instances For

source
@[simp]
theorem ENNReal.toNNReal_pow (a : ENNReal) (n : ℕ) :
(a ^ n).toNNReal = a.toNNReal ^ n
source
def ENNReal.toRealHom :
ENNReal →*₀ ℝ

`ENNReal.toReal` as a `MonoidHom`.

Equations

- ENNReal.toRealHom = (↑NNReal.toRealHom).comp ENNReal.toNNRealHom

Instances For

source
@[simp]
theorem ENNReal.toReal_mul {a b : ENNReal} :
(a * b).toReal = a.toReal * b.toReal
source
theorem ENNReal.toReal_nsmul (a : ENNReal) (n : ℕ) :
(n • a).toReal = n • a.toReal
source
@[simp]
theorem ENNReal.toReal_pow (a : ENNReal) (n : ℕ) :
(a ^ n).toReal = a.toReal ^ n
source
theorem ENNReal.toReal_ofReal_mul (c : ℝ) (a : ENNReal) (h : 0 ≤ c) :
(ENNReal.ofReal c * a).toReal = c * a.toReal
source
theorem ENNReal.toReal_mul_top (a : ENNReal) :
(a * ⊤).toReal = 0
source
theorem ENNReal.toReal_top_mul (a : ENNReal) :
(⊤ * a).toReal = 0
source
@[deprecated ENNReal.toReal_eq_toReal_iff' (since := "2025-11-07")]
theorem ENNReal.toReal_eq_toReal {x y : ENNReal} (hx : x ≠ ⊤) (hy : y ≠ ⊤) :
x.toReal = y.toReal ↔ x = y

Alias of `ENNReal.toReal_eq_toReal_iff'`.

source
theorem ENNReal.trichotomy (p : ENNReal) :
p = 0 ∨ p = ⊤ ∨ 0 < p.toReal
source
theorem ENNReal.trichotomy₂ {p q : ENNReal} (hpq : p ≤ q) :
p = 0 ∧ q = 0 ∨ p = 0 ∧ q = ⊤ ∨ p = 0 ∧ 0 < q.toReal ∨ p = ⊤ ∧ q = ⊤ ∨ 0 < p.toReal ∧ q = ⊤ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal
source
theorem ENNReal.dichotomy (p : ENNReal) [Fact (1 ≤ p)] :
p = ⊤ ∨ 1 ≤ p.toReal
source
theorem ENNReal.toReal_pos_iff_ne_top (p : ENNReal) [Fact (1 ≤ p)] :
0 < p.toReal ↔ p ≠ ⊤
source
@[deprecated ENNReal.max_eq_zero_iff (since := "2025-10-25")]
theorem ENNReal.sup_eq_zero {a b : ENNReal} :
max a b = 0 ↔ a = 0 ∧ b = 0
source
def Mathlib.Meta.Positivity.evalENNRealOfReal :
PositivityExt

Extension for the `positivity` tactic: `ENNReal.ofReal`.

Equations

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

Instances For