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.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.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_nat_cast {p : } {n : } (hn : n 0) :
ENNReal.ofReal p < n p < n
@[simp]
@[simp]
theorem ENNReal.nat_cast_le_ofReal {n : } {p : } (hn : n 0) :
n ENNReal.ofReal p n p
@[simp]
@[simp]
theorem ENNReal.ofReal_le_nat_cast {r : } {n : } :
ENNReal.ofReal r n r n
@[simp]
@[simp]
theorem ENNReal.nat_cast_lt_ofReal {n : } {r : } :
n < ENNReal.ofReal r n < r
@[simp]
@[simp]
theorem ENNReal.ofReal_eq_nat_cast {r : } {n : } (h : n 0) :
ENNReal.ofReal r = n r = n
@[simp]
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

ENNReal.toNNReal as a MonoidHom.

Equations
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} :
    (Finset.prod s fun (i : ι) => f i).toNNReal = Finset.prod s fun (i : ι) => (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} :
    (Finset.prod s fun (i : ι) => f i).toReal = Finset.prod s fun (i : ι) => (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 (Finset.prod s fun (i : α) => f i) = Finset.prod s fun (i : α) => 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 = ⨅ 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 : ι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 : ι), Finset.sum s fun (a : α) => f i a) = Finset.sum s fun (a : α) => ⨅ (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_coe_nat :
    ⨆ (n : ), n =