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 #

theorem ENNReal.toReal_add {a : ENNReal} {b : ENNReal} (ha : a ) (hb : b ) :
(a + b).toReal = a.toReal + b.toReal
theorem ENNReal.toReal_sub_of_le {a : ENNReal} {b : ENNReal} (h : b a) (ha : a ) :
(a - b).toReal = a.toReal - b.toReal
theorem ENNReal.le_toReal_sub {a : ENNReal} {b : ENNReal} (hb : b ) :
a.toReal - b.toReal (a - b).toReal
theorem ENNReal.toReal_add_le {a : ENNReal} {b : ENNReal} :
(a + b).toReal a.toReal + b.toReal
theorem ENNReal.ofReal_add {p : } {q : } (hp : 0 p) (hq : 0 q) :
@[simp]
theorem ENNReal.toReal_le_toReal {a : ENNReal} {b : ENNReal} (ha : a ) (hb : b ) :
a.toReal b.toReal a b
theorem ENNReal.toReal_mono {a : ENNReal} {b : ENNReal} (hb : b ) (h : a b) :
a.toReal b.toReal
theorem ENNReal.toReal_mono' {a : ENNReal} {b : ENNReal} (h : a b) (ht : b = a = ) :
a.toReal b.toReal
@[simp]
theorem ENNReal.toReal_lt_toReal {a : ENNReal} {b : ENNReal} (ha : a ) (hb : b ) :
a.toReal < b.toReal a < b
theorem ENNReal.toReal_strict_mono {a : ENNReal} {b : ENNReal} (hb : b ) (h : a < b) :
a.toReal < b.toReal
theorem ENNReal.toNNReal_mono {a : ENNReal} {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 : ENNReal} {b : ENNReal} {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 : ENNReal} {b : ENNReal} {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 : ENNReal} {b : ENNReal} (ha : a ) (hb : b ) :
a.toNNReal b.toNNReal a b
theorem ENNReal.toNNReal_strict_mono {a : ENNReal} {b : ENNReal} (hb : b ) (h : a < b) :
a.toNNReal < b.toNNReal
@[simp]
theorem ENNReal.toNNReal_lt_toNNReal {a : ENNReal} {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) :
a.toNNReal < p
theorem ENNReal.toReal_max {a : ENNReal} {b : ENNReal} (hr : a ) (hp : b ) :
(max a b).toReal = max a.toReal b.toReal
theorem ENNReal.toReal_min {a : ENNReal} {b : ENNReal} (hr : a ) (hp : b ) :
(min a b).toReal = min a.toReal b.toReal
theorem ENNReal.toReal_sup {a : ENNReal} {b : ENNReal} :
a b (a b).toReal = a.toReal b.toReal
theorem ENNReal.toReal_inf {a : ENNReal} {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 ) :
0 < a.toNNReal
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 ) :
0 < a.toReal
theorem ENNReal.ofReal_le_of_le_toReal {a : } {b : ENNReal} (h : a b.toReal) :
@[simp]
@[simp]
theorem ENNReal.ofReal_eq_ofReal_iff {p : } {q : } (hp : 0 p) (hq : 0 q) :
@[simp]
theorem ENNReal.ofReal_lt_ofReal_iff {p : } {q : } (h : 0 < q) :
@[simp]
theorem ENNReal.ofReal_pos {p : } :
@[simp]
@[simp]
theorem ENNReal.ofReal_of_nonpos {p : } :
p 0ENNReal.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
@[deprecated ENNReal.ofReal_lt_natCast]
theorem ENNReal.ofReal_lt_nat_cast {p : } {n : } (hn : n 0) :
ENNReal.ofReal p < n p < n

Alias of ENNReal.ofReal_lt_natCast.

@[simp]
@[simp]
theorem ENNReal.ofReal_lt_ofNat {p : } {n : } [n.AtLeastTwo] :
@[simp]
theorem ENNReal.natCast_le_ofReal {n : } {p : } (hn : n 0) :
n ENNReal.ofReal p n p
@[deprecated ENNReal.natCast_le_ofReal]
theorem ENNReal.nat_cast_le_ofReal {n : } {p : } (hn : n 0) :
n ENNReal.ofReal p n p

Alias of ENNReal.natCast_le_ofReal.

@[simp]
@[simp]
theorem ENNReal.ofNat_le_ofReal {n : } [n.AtLeastTwo] {p : } :
@[simp]
theorem ENNReal.ofReal_le_natCast {r : } {n : } :
ENNReal.ofReal r n r n
@[deprecated ENNReal.ofReal_le_natCast]
theorem ENNReal.ofReal_le_nat_cast {r : } {n : } :
ENNReal.ofReal r n r n

Alias of ENNReal.ofReal_le_natCast.

@[simp]
@[simp]
theorem ENNReal.ofReal_le_ofNat {r : } {n : } [n.AtLeastTwo] :
@[simp]
theorem ENNReal.natCast_lt_ofReal {n : } {r : } :
n < ENNReal.ofReal r n < r
@[deprecated ENNReal.natCast_lt_ofReal]
theorem ENNReal.nat_cast_lt_ofReal {n : } {r : } :
n < ENNReal.ofReal r n < r

Alias of ENNReal.natCast_lt_ofReal.

@[simp]
@[simp]
theorem ENNReal.ofNat_lt_ofReal {n : } [n.AtLeastTwo] {r : } :
@[simp]
theorem ENNReal.ofReal_eq_natCast {r : } {n : } (h : n 0) :
ENNReal.ofReal r = n r = n
@[deprecated ENNReal.ofReal_eq_natCast]
theorem ENNReal.ofReal_eq_nat_cast {r : } {n : } (h : n 0) :
ENNReal.ofReal r = n r = n

Alias of ENNReal.ofReal_eq_natCast.

@[simp]
@[simp]
theorem ENNReal.ofReal_eq_ofNat {r : } {n : } [n.AtLeastTwo] :
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) :
a.toReal 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) :
a.toReal < b
theorem ENNReal.ofReal_pow {p : } (hp : 0 p) (n : ) :
@[simp]
theorem ENNReal.toNNReal_mul {a : ENNReal} {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
@[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} :
(is, f i).toNNReal = is, (f i).toNNReal
@[simp]
theorem ENNReal.toReal_mul {a : ENNReal} {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} :
(is, f i).toReal = is, (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 : ENNReal} {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 : ENNReal} {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
theorem ENNReal.toNNReal_inv (a : ENNReal) :
a⁻¹.toNNReal = a.toNNReal⁻¹
theorem ENNReal.toNNReal_div (a : ENNReal) (b : ENNReal) :
(a / b).toNNReal = a.toNNReal / b.toNNReal
theorem ENNReal.toReal_inv (a : ENNReal) :
a⁻¹.toReal = a.toReal⁻¹
theorem ENNReal.toReal_div (a : ENNReal) (b : ENNReal) :
(a / b).toReal = a.toReal / b.toReal
theorem ENNReal.ofReal_prod_of_nonneg {α : Type u_1} {s : Finset α} {f : α} (hf : is, 0 f i) :
ENNReal.ofReal (is, f i) = is, 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 : rs, 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 : rs, 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 : rs, 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 : rs, r ) :
(sSup s).toReal = sSup (ENNReal.toReal '' s)
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 = bs, 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 : ιENNReal} {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 : ι), at, f k a f i a f k a f j a) :
⨅ (i : ι), as, f i a = as, ⨅ (i : ι), f i a
theorem ENNReal.iInf_mul_of_ne {ι : Sort u_2} {f : ιENNReal} {x : ENNReal} (h0 : x 0) (h : x ) :
iInf f * x = ⨅ (i : ι), f i * x

If x ≠ 0 and x ≠ ∞, then right multiplication by x maps infimum to infimum. See also ENNReal.iInf_mul that assumes [Nonempty ι] but does not require x ≠ 0.

theorem ENNReal.iInf_mul {ι : Sort u_2} [Nonempty ι] {f : ιENNReal} {x : ENNReal} (h : x ) :
iInf f * x = ⨅ (i : ι), f i * x

If x ≠ ∞, then right multiplication by x maps infimum over a nonempty type to infimum. See also ENNReal.iInf_mul_of_ne that assumes x ≠ 0 but does not require [Nonempty ι].

theorem ENNReal.mul_iInf {ι : Sort u_2} [Nonempty ι] {f : ιENNReal} {x : ENNReal} (h : x ) :
x * iInf f = ⨅ (i : ι), x * f i

If x ≠ ∞, then left multiplication by x maps infimum over a nonempty type to infimum. See also ENNReal.mul_iInf_of_ne that assumes x ≠ 0 but does not require [Nonempty ι].

theorem ENNReal.mul_iInf_of_ne {ι : Sort u_2} {f : ιENNReal} {x : ENNReal} (h0 : x 0) (h : x ) :
x * iInf f = ⨅ (i : ι), x * f i

If x ≠ 0 and x ≠ ∞, then left multiplication by x maps infimum to infimum. See also ENNReal.mul_iInf that assumes [Nonempty ι] but does not require x ≠ 0.

supr_mul, mul_supr and variants are in Topology.Instances.ENNReal.

@[simp]
theorem ENNReal.iSup_eq_zero {ι : Sort u_1} {f : ιENNReal} :
⨆ (i : ι), f i = 0 ∀ (i : ι), f i = 0
@[simp]
theorem ENNReal.iSup_zero_eq_zero {ι : Sort u_1} :
⨆ (x : ι), 0 = 0
theorem ENNReal.sup_eq_zero {a : ENNReal} {b : ENNReal} :
a b = 0 a = 0 b = 0
theorem ENNReal.iSup_natCast :
⨆ (n : ), n =
@[deprecated ENNReal.iSup_natCast]
theorem ENNReal.iSup_coe_nat :
⨆ (n : ), n =

Alias of ENNReal.iSup_natCast.