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 b : ENNReal} (ha : a ) (hb : b ) :
(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 b : ENNReal} (ha : a ) (hb : b ) :
theorem ENNReal.toReal_mono {a b : ENNReal} (hb : b ) (h : a b) :
theorem ENNReal.toReal_mono' {a b : ENNReal} (h : a b) (ht : b = a = ) :
@[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) :
theorem ENNReal.toNNReal_mono {a b : ENNReal} (hb : b ) (h : a b) :
theorem ENNReal.le_toNNReal_of_coe_le {a : ENNReal} {p : NNReal} (h : p a) (ha : a ) :
@[simp]
theorem ENNReal.toNNReal_le_toNNReal {a b : ENNReal} (ha : a ) (hb : b ) :
theorem ENNReal.toNNReal_strict_mono {a b : ENNReal} (hb : b ) (h : a < b) :
@[simp]
theorem ENNReal.toNNReal_lt_toNNReal {a b : ENNReal} (ha : a ) (hb : 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 ) :
theorem ENNReal.toReal_min {a b : ENNReal} (hr : a ) (hp : b ) :
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 {a : ENNReal} (ha₀ : a 0) (ha_top : a ) :
theorem ENNReal.toReal_pos {a : ENNReal} (ha₀ : a 0) (ha_top : a ) :
0 < a.toReal
@[simp]
theorem ENNReal.ofReal_eq_ofReal_iff {p q : } (hp : 0 p) (hq : 0 q) :
@[simp]
@[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
@[simp]
@[simp]
theorem ENNReal.natCast_le_ofReal {n : } {p : } (hn : n 0) :
n ENNReal.ofReal p n p
@[simp]
@[simp]
theorem ENNReal.ofReal_le_natCast {r : } {n : } :
ENNReal.ofReal r n r n
@[simp]
@[simp]
theorem ENNReal.natCast_lt_ofReal {n : } {r : } :
n < ENNReal.ofReal r n < r
@[simp]
@[simp]
theorem ENNReal.ofReal_eq_natCast {r : } {n : } (h : n 0) :
ENNReal.ofReal r = n r = n
@[simp]
theorem ENNReal.ofReal_lt_iff_lt_toReal {a : } {b : ENNReal} (ha : 0 a) (hb : 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) :
theorem ENNReal.toReal_le_of_le_ofReal {a : ENNReal} {b : } (hb : 0 b) (h : a ENNReal.ofReal b) :
theorem ENNReal.ofReal_pow {p : } (hp : 0 p) (n : ) :
@[simp]
@[simp]
theorem ENNReal.toNNReal_pow (a : ENNReal) (n : ) :
(a ^ n).toNNReal = a.toNNReal ^ n
@[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) :
theorem ENNReal.toReal_eq_toReal {a b : ENNReal} (ha : a ) (hb : b ) :
a.toReal = b.toReal a = b
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)] :
theorem ENNReal.sup_eq_zero {a b : ENNReal} :
max a b = 0 a = 0 b = 0

Extension for the positivity tactic: ENNReal.ofReal.

Equations
  • One or more equations did not get rendered due to their size.
Instances For