Documentation

Mathlib.Data.ENNReal.Real

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.

theorem ENNReal.toReal_add {a b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :

(a + b).toReal = a.toReal + b.toReal

theorem ENNReal.toReal_add_le {a b : ENNReal} :

(a + b).toReal ≤ a.toReal + b.toReal

theorem ENNReal.ofReal_add {p q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) :

ENNReal.ofReal (p + q) = ENNReal.ofReal p + ENNReal.ofReal q

theorem ENNReal.ofReal_add_le {p q : ℝ} :

ENNReal.ofReal (p + q) ≤ ENNReal.ofReal p + ENNReal.ofReal q

@[simp]

theorem ENNReal.toReal_le_toReal {a b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :

a.toReal ≤ b.toReal ↔ a ≤ b

theorem ENNReal.toReal_mono {a b : ENNReal} (hb : b ≠ ⊤) (h : a ≤ b) :

a.toReal ≤ b.toReal

theorem ENNReal.toReal_mono' {a b : ENNReal} (h : a ≤ b) (ht : b = ⊤ → a = ⊤) :

a.toReal ≤ b.toReal

@[simp]

theorem ENNReal.toReal_lt_toReal {a b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :

a.toReal < b.toReal ↔ a < b

theorem ENNReal.toReal_strict_mono {a b : ENNReal} (hb : b ≠ ⊤) (h : a < b) :

a.toReal < b.toReal

theorem ENNReal.toNNReal_mono {a b : ENNReal} (hb : b ≠ ⊤) (h : a ≤ b) :

a.toNNReal ≤ b.toNNReal

theorem ENNReal.le_toNNReal_of_coe_le {a : ENNReal} {p : NNReal} (h : ↑p ≤ a) (ha : a ≠ ⊤) :

p ≤ a.toNNReal

@[simp]

theorem ENNReal.toNNReal_le_toNNReal {a b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :

a.toNNReal ≤ b.toNNReal ↔ a ≤ b

theorem ENNReal.toNNReal_strict_mono {a b : ENNReal} (hb : b ≠ ⊤) (h : a < b) :

a.toNNReal < b.toNNReal

@[simp]

theorem ENNReal.toNNReal_lt_toNNReal {a b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :

a.toNNReal < b.toNNReal ↔ a < b

theorem ENNReal.toNNReal_lt_of_lt_coe {a : ENNReal} {p : NNReal} (h : a < ↑p) :

theorem ENNReal.toReal_max {a b : ENNReal} (hr : a ≠ ⊤) (hp : b ≠ ⊤) :

(max a b).toReal = max a.toReal b.toReal

theorem ENNReal.toReal_min {a b : ENNReal} (hr : a ≠ ⊤) (hp : b ≠ ⊤) :

(min a b).toReal = min a.toReal b.toReal

theorem ENNReal.toReal_sup {a b : ENNReal} :

a ≠ ⊤ → b ≠ ⊤ → (max a b).toReal = max a.toReal b.toReal

theorem ENNReal.toReal_inf {a b : ENNReal} :

a ≠ ⊤ → b ≠ ⊤ → (min a b).toReal = min a.toReal b.toReal

theorem ENNReal.toNNReal_pos_iff {a : ENNReal} :

0 < a.toNNReal ↔ 0 < a ∧ a < ⊤

theorem ENNReal.toNNReal_pos {a : ENNReal} (ha₀ : a ≠ 0) (ha_top : a ≠ ⊤) :

theorem ENNReal.toReal_pos_iff {a : ENNReal} :

0 < a.toReal ↔ 0 < a ∧ a < ⊤

theorem ENNReal.toReal_pos {a : ENNReal} (ha₀ : a ≠ 0) (ha_top : a ≠ ⊤) :

theorem ENNReal.ofReal_le_ofReal {p q : ℝ} (h : p ≤ q) :

ENNReal.ofReal p ≤ ENNReal.ofReal q

theorem ENNReal.ofReal_mono :

Monotone ENNReal.ofReal

theorem ENNReal.ofReal_le_of_le_toReal {a : ℝ} {b : ENNReal} (h : a ≤ b.toReal) :

ENNReal.ofReal a ≤ b

@[simp]

theorem ENNReal.ofReal_le_ofReal_iff {p q : ℝ} (h : 0 ≤ q) :

ENNReal.ofReal p ≤ ENNReal.ofReal q ↔ p ≤ q

theorem ENNReal.ofReal_le_ofReal_iff' {p q : ℝ} :

ENNReal.ofReal p ≤ ENNReal.ofReal q ↔ p ≤ q ∨ p ≤ 0

@[simp]

theorem ENNReal.ofReal_le_coe {a : ℝ} {b : NNReal} :

ENNReal.ofReal a ≤ ↑b ↔ a ≤ ↑b

theorem ENNReal.ofReal_lt_ofReal_iff' {p q : ℝ} :

ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q ∧ 0 < q

@[simp]

theorem ENNReal.ofReal_eq_ofReal_iff {p q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) :

ENNReal.ofReal p = ENNReal.ofReal q ↔ p = q

@[simp]

theorem ENNReal.ofReal_lt_ofReal_iff {p q : ℝ} (h : 0 < q) :

ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q

theorem ENNReal.ofReal_lt_ofReal_iff_of_nonneg {p q : ℝ} (hp : 0 ≤ p) :

ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q

@[simp]

theorem ENNReal.ofReal_pos {p : ℝ} :

0 < ENNReal.ofReal p ↔ 0 < p

@[simp]

theorem ENNReal.ofReal_eq_zero {p : ℝ} :

ENNReal.ofReal p = 0 ↔ p ≤ 0

@[simp]

theorem ENNReal.ofReal_min (x y : ℝ) :

ENNReal.ofReal (min x y) = min (ENNReal.ofReal x) (ENNReal.ofReal y)

@[simp]

theorem ENNReal.ofReal_max (x y : ℝ) :

ENNReal.ofReal (max x y) = max (ENNReal.ofReal x) (ENNReal.ofReal y)

theorem ENNReal.ofReal_ne_zero_iff {r : ℝ} :

ENNReal.ofReal r ≠ 0 ↔ 0 < r

@[simp]

theorem ENNReal.zero_eq_ofReal {p : ℝ} :

0 = ENNReal.ofReal p ↔ p ≤ 0

theorem ENNReal.ofReal_of_nonpos {p : ℝ} :

p ≤ 0 → ENNReal.ofReal p = 0

Alias of the reverse direction of ENNReal.ofReal_eq_zero.

@[simp]

theorem ENNReal.ofReal_lt_natCast {p : ℝ} {n : ℕ} (hn : n ≠ 0) :

ENNReal.ofReal p < ↑n ↔ p < ↑n

@[simp]

theorem ENNReal.ofReal_lt_one {p : ℝ} :

ENNReal.ofReal p < 1 ↔ p < 1

@[simp]

theorem ENNReal.ofReal_lt_ofNat {p : ℝ} {n : ℕ} [n.AtLeastTwo] :

ENNReal.ofReal p < OfNat.ofNat n ↔ p < OfNat.ofNat n

@[simp]

theorem ENNReal.natCast_le_ofReal {n : ℕ} {p : ℝ} (hn : n ≠ 0) :

↑n ≤ ENNReal.ofReal p ↔ ↑n ≤ p

@[simp]

theorem ENNReal.one_le_ofReal {p : ℝ} :

1 ≤ ENNReal.ofReal p ↔ 1 ≤ p

@[simp]

theorem ENNReal.ofNat_le_ofReal {n : ℕ} [n.AtLeastTwo] {p : ℝ} :

OfNat.ofNat n ≤ ENNReal.ofReal p ↔ OfNat.ofNat n ≤ p

@[simp]

theorem ENNReal.ofReal_le_natCast {r : ℝ} {n : ℕ} :

ENNReal.ofReal r ≤ ↑n ↔ r ≤ ↑n

@[simp]

theorem ENNReal.ofReal_le_one {r : ℝ} :

ENNReal.ofReal r ≤ 1 ↔ r ≤ 1

@[simp]

theorem ENNReal.ofReal_le_ofNat {r : ℝ} {n : ℕ} [n.AtLeastTwo] :

ENNReal.ofReal r ≤ OfNat.ofNat n ↔ r ≤ OfNat.ofNat n

@[simp]

theorem ENNReal.natCast_lt_ofReal {n : ℕ} {r : ℝ} :

↑n < ENNReal.ofReal r ↔ ↑n < r

@[simp]

theorem ENNReal.one_lt_ofReal {r : ℝ} :

1 < ENNReal.ofReal r ↔ 1 < r

@[simp]

theorem ENNReal.ofNat_lt_ofReal {n : ℕ} [n.AtLeastTwo] {r : ℝ} :

OfNat.ofNat n < ENNReal.ofReal r ↔ OfNat.ofNat n < r

@[simp]

theorem ENNReal.ofReal_eq_natCast {r : ℝ} {n : ℕ} (h : n ≠ 0) :

ENNReal.ofReal r = ↑n ↔ r = ↑n

@[simp]

theorem ENNReal.ofReal_eq_one {r : ℝ} :

ENNReal.ofReal r = 1 ↔ r = 1

@[simp]

theorem ENNReal.ofReal_eq_ofNat {r : ℝ} {n : ℕ} [n.AtLeastTwo] :

ENNReal.ofReal r = OfNat.ofNat n ↔ r = OfNat.ofNat n

theorem ENNReal.ofReal_le_iff_le_toReal {a : ℝ} {b : ENNReal} (hb : b ≠ ⊤) :

ENNReal.ofReal a ≤ b ↔ a ≤ b.toReal

theorem ENNReal.ofReal_lt_iff_lt_toReal {a : ℝ} {b : ENNReal} (ha : 0 ≤ a) (hb : b ≠ ⊤) :

ENNReal.ofReal a < b ↔ a < b.toReal

@[simp]

theorem ENNReal.coe_lt_ofReal {a : NNReal} {b : ℝ} :

↑a < ENNReal.ofReal b ↔ ↑a < b

theorem ENNReal.ofReal_lt_coe_iff {a : ℝ} {b : NNReal} (ha : 0 ≤ a) :

ENNReal.ofReal a < ↑b ↔ a < ↑b

theorem ENNReal.le_ofReal_iff_toReal_le {a : ENNReal} {b : ℝ} (ha : a ≠ ⊤) (hb : 0 ≤ b) :

a ≤ ENNReal.ofReal b ↔ a.toReal ≤ b

theorem ENNReal.toReal_le_of_le_ofReal {a : ENNReal} {b : ℝ} (hb : 0 ≤ b) (h : a ≤ ENNReal.ofReal b) :

theorem ENNReal.lt_ofReal_iff_toReal_lt {a : ENNReal} {b : ℝ} (ha : a ≠ ⊤) :

a < ENNReal.ofReal b ↔ a.toReal < b

theorem ENNReal.toReal_lt_of_lt_ofReal {a : ENNReal} {b : ℝ} (h : a < ENNReal.ofReal b) :

@[simp]

theorem ENNReal.ofReal_mul {p q : ℝ} (hp : 0 ≤ p) :

ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q

theorem ENNReal.ofReal_mul' {p q : ℝ} (hq : 0 ≤ q) :

ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q

@[simp]

theorem ENNReal.ofReal_pow {p : ℝ} (hp : 0 ≤ p) (n : ℕ) :

ENNReal.ofReal (p ^ n) = ENNReal.ofReal p ^ n

theorem ENNReal.ofReal_nsmul {x : ℝ} {n : ℕ} :

ENNReal.ofReal (n • x) = n • ENNReal.ofReal x

@[simp]

theorem ENNReal.toNNReal_mul {a b : ENNReal} :

(a * b).toNNReal = a.toNNReal * b.toNNReal

theorem ENNReal.toNNReal_mul_top (a : ENNReal) :

(a * ⊤).toNNReal = 0

theorem ENNReal.toNNReal_top_mul (a : ENNReal) :

(⊤ * a).toNNReal = 0

noncomputable def ENNReal.toNNRealHom :

ENNReal →*₀ NNReal

ENNReal.toNNReal as a MonoidHom.

Instances For

@[simp]

theorem ENNReal.toNNReal_pow (a : ENNReal) (n : ℕ) :

(a ^ n).toNNReal = a.toNNReal ^ n

noncomputable def ENNReal.toRealHom :

ENNReal →*₀ ℝ

ENNReal.toReal as a MonoidHom.

Instances For

@[simp]

theorem ENNReal.toReal_mul {a b : ENNReal} :

(a * b).toReal = a.toReal * b.toReal

theorem ENNReal.toReal_nsmul (a : ENNReal) (n : ℕ) :

(n • a).toReal = n • a.toReal

@[simp]

theorem ENNReal.toReal_pow (a : ENNReal) (n : ℕ) :

(a ^ n).toReal = a.toReal ^ n

theorem ENNReal.toReal_ofReal_mul (c : ℝ) (a : ENNReal) (h : 0 ≤ c) :

(ENNReal.ofReal c * a).toReal = c * a.toReal

theorem ENNReal.toReal_mul_top (a : ENNReal) :

(a * ⊤).toReal = 0

theorem ENNReal.toReal_top_mul (a : ENNReal) :

(⊤ * a).toReal = 0

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

theorem ENNReal.trichotomy (p : ENNReal) :

p = 0 ∨ p = ⊤ ∨ 0 < p.toReal

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

theorem ENNReal.dichotomy (p : ENNReal) [Fact (1 ≤ p)] :

p = ⊤ ∨ 1 ≤ p.toReal

theorem ENNReal.toReal_pos_iff_ne_top (p : ENNReal) [Fact (1 ≤ p)] :

0 < p.toReal ↔ p ≠ ⊤

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

def Mathlib.Meta.Positivity.evalENNRealOfReal :

Extension for the positivity tactic: ENNReal.ofReal.

Instances For