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 theorems #

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_sub_of_le {a b : ENNReal} (h : b ≤ a) (ha : a ≠ ⊤) :

(a - b).toReal = a.toReal - b.toReal

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

a.toReal - b.toReal ≤ (a - 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

theorem ENNReal.toReal_le_add' {a b c : ENNReal} (hle : a ≤ b + c) (hb : b = ⊤ → a = ⊤) (hc : c = ⊤ → a = ⊤) :

a.toReal ≤ b.toReal + c.toReal

If a ≤ b + c and a = ∞ whenever b = ∞ or c = ∞, then ENNReal.toReal a ≤ ENNReal.toReal b + ENNReal.toReal c. This lemma is useful to transfer triangle-like inequalities from ENNReals to Reals.

theorem ENNReal.toReal_le_add {a b c : ENNReal} (hle : a ≤ b + c) (hb : b ≠ ⊤) (hc : c ≠ ⊤) :

a.toReal ≤ b.toReal + c.toReal

If a ≤ b + c, b ≠ ∞, and c ≠ ∞, then ENNReal.toReal a ≤ ENNReal.toReal b + ENNReal.toReal c. This lemma is useful to transfer triangle-like inequalities from ENNReals to Reals.

@[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 ≠ ⊤) :

(a ⊔ b).toReal = a.toReal ⊔ b.toReal

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

(a ⊓ b).toReal = a.toReal ⊓ b.toReal

theorem ENNReal.toReal_sup {a b : ENNReal} :

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

theorem ENNReal.toReal_inf {a b : ENNReal} :

a ≠ ⊤ → b ≠ ⊤ → (a ⊓ b).toReal = 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_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

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.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_sub (p : ℝ) {q : ℝ} (hq : 0 ≤ q) :

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

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

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

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

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

theorem ENNReal.ofReal_inv_of_pos {x : ℝ} (hx : 0 < x) :

ENNReal.ofReal x ⁻¹ = (ENNReal.ofReal x)⁻¹

theorem ENNReal.ofReal_div_of_pos {x y : ℝ} (hy : 0 < y) :

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

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

@[simp]

theorem ENNReal.smul_toNNReal (a : NNReal) (b : ENNReal) :

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

def ENNReal.toNNRealHom :

ENNReal →* NNReal

ENNReal.toNNReal as a MonoidHom.

Equations

ENNReal.toNNRealHom = { toFun := ENNReal.toNNReal, map_one' := ENNReal.toNNRealHom.proof_1, map_mul' := ⋯ }

Instances For

@[simp]

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

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

@[simp]

theorem ENNReal.toNNReal_prod {ι : Type u_1} {s : Finset ι} {f : ι → ENNReal} :

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

def ENNReal.toRealHom :

ENNReal →* ℝ

ENNReal.toReal as a MonoidHom.

Equations

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

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

@[simp]

theorem ENNReal.toReal_prod {ι : Type u_1} {s : Finset ι} {f : ι → ENNReal} :

(∏ i ∈ s, f i).toReal = ∏ i ∈ s, (f i).toReal

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

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

a.toReal = b.toReal ↔ a = b

theorem ENNReal.toReal_smul (r : NNReal) (s : ENNReal) :

(r • s).toReal = r • s.toReal

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 ≠ ⊤

@[simp]

theorem ENNReal.toNNReal_inv (a : ENNReal) :

a ⁻¹.toNNReal = a.toNNReal ⁻¹

@[simp]

theorem ENNReal.toNNReal_div (a b : ENNReal) :

(a / b).toNNReal = a.toNNReal / b.toNNReal

@[simp]

theorem ENNReal.toReal_inv (a : ENNReal) :

a ⁻¹.toReal = a.toReal ⁻¹

@[simp]

theorem ENNReal.toReal_div (a b : ENNReal) :

(a / b).toReal = a.toReal / b.toReal

theorem ENNReal.ofReal_prod_of_nonneg {α : Type u_1} {s : Finset α} {f : α → ℝ} (hf : ∀ i ∈ s, 0 ≤ f i) :

ENNReal.ofReal (∏ i ∈ s, f i) = ∏ i ∈ s, ENNReal.ofReal (f i)

theorem ENNReal.toNNReal_iInf {ι : Sort u_1} {f : ι → ENNReal} (hf : ∀ (i : ι), f i ≠ ⊤) :

(iInf f).toNNReal = ⨅ (i : ι), (f i).toNNReal

theorem ENNReal.toNNReal_sInf (s : Set ENNReal) (hs : ∀ r ∈ s, r ≠ ⊤) :

(sInf s).toNNReal = sInf (ENNReal.toNNReal '' s)

theorem ENNReal.toNNReal_iSup {ι : Sort u_1} {f : ι → ENNReal} (hf : ∀ (i : ι), f i ≠ ⊤) :

(iSup f).toNNReal = ⨆ (i : ι), (f i).toNNReal

theorem ENNReal.toNNReal_sSup (s : Set ENNReal) (hs : ∀ r ∈ s, r ≠ ⊤) :

(sSup s).toNNReal = sSup (ENNReal.toNNReal '' s)

theorem ENNReal.toReal_iInf {ι : Sort u_1} {f : ι → ENNReal} (hf : ∀ (i : ι), f i ≠ ⊤) :

(iInf f).toReal = ⨅ (i : ι), (f i).toReal

theorem ENNReal.toReal_sInf (s : Set ENNReal) (hf : ∀ r ∈ s, r ≠ ⊤) :

(sInf s).toReal = sInf (ENNReal.toReal '' s)

theorem ENNReal.toReal_iSup {ι : Sort u_1} {f : ι → ENNReal} (hf : ∀ (i : ι), f i ≠ ⊤) :

(iSup f).toReal = ⨆ (i : ι), (f i).toReal

theorem ENNReal.toReal_sSup (s : Set ENNReal) (hf : ∀ r ∈ s, r ≠ ⊤) :

(sSup s).toReal = sSup (ENNReal.toReal '' s)

@[simp]

theorem ENNReal.ofReal_iInf {ι : Sort u_1} [Nonempty ι] (f : ι → ℝ) :

ENNReal.ofReal (⨅ (i : ι), f i) = ⨅ (i : ι), ENNReal.ofReal (f i)

theorem ENNReal.iInf_add {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal} :

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

theorem ENNReal.iSup_sub {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal} :

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

theorem ENNReal.sub_iInf {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal} :

a - ⨅ (i : ι), f i = ⨆ (i : ι), a - f i

theorem ENNReal.sInf_add {a : ENNReal} {s : Set ENNReal} :

sInf s + a = ⨅ b ∈ s, b + a

theorem ENNReal.add_iInf {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal} :

a + iInf f = ⨅ (b : ι), a + f b

theorem ENNReal.iInf_add_iInf {ι : Sort u_1} {f g : ι → ENNReal} (h : ∀ (i j : ι), ∃ (k : ι), f k + g k ≤ f i + g j) :

iInf f + iInf g = ⨅ (a : ι), f a + g a

theorem ENNReal.iInf_sum {ι : Sort u_1} {α : Type u_2} {f : ι → α → ENNReal} {s : Finset α} [Nonempty ι] (h : ∀ (t : Finset α) (i j : ι), ∃ (k : ι), ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a) :

⨅ (i : ι), ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ (i : ι), f i a

theorem ENNReal.sup_eq_zero {a b : ENNReal} :

a ⊔ b = 0 ↔ a = 0 ∧ b = 0

def Mathlib.Meta.Positivity.evalENNRealOfReal :

Extension for the positivity tactic: ENNReal.ofReal.

Instances For