# Extended non-negative reals #

We define ENNReal = ℝ≥0∞ := WithTop ℝ≥0 to be the type of extended nonnegative real numbers, i.e., the interval [0, +∞]. This type is used as the codomain of a MeasureTheory.Measure, and of the extended distance edist in an EMetricSpace.

In this file we set up many of the instances on ℝ≥0∞, and provide relationships between ℝ≥0∞ and ℝ≥0, and between ℝ≥0∞ and . In particular, we provide a coercion from ℝ≥0 to ℝ≥0∞ as well as functions ENNReal.toNNReal, ENNReal.ofReal and ENNReal.toReal, all of which take the value zero wherever they cannot be the identity. Also included is the relationship between ℝ≥0∞ and . The interaction of these functions, especially ENNReal.ofReal and ENNReal.toReal, with the algebraic and lattice structure can be found in Data.ENNReal.Real.

This file proves many of the order properties of ℝ≥0∞, with the exception of the ways those relate to the algebraic structure, which are included in Data.ENNReal.Operations. This file also defines inversion and division: this includes Inv and Div instances on ℝ≥0∞ making it into a DivInvOneMonoid. As a consequence of being a DivInvOneMonoid, ℝ≥0∞ inherits a power operation with integer exponent: this and other properties is shown in Data.ENNReal.Inv.

## Main definitions #

• ℝ≥0∞: the extended nonnegative real numbers [0, ∞]; defined as WithTop ℝ≥0; it is equipped with the following structures:

• coercion from ℝ≥0 defined in the natural way;

• the natural structure of a complete dense linear order: ↑p ≤ ↑q ↔ p ≤ q and ∀ a, a ≤ ∞;

• a + b is defined so that ↑p + ↑q = ↑(p + q) for (p q : ℝ≥0) and a + ∞ = ∞ + a = ∞;

• a * b is defined so that ↑p * ↑q = ↑(p * q) for (p q : ℝ≥0), 0 * ∞ = ∞ * 0 = 0, and a * ∞ = ∞ * a = ∞ for a ≠ 0;

• a - b is defined as the minimal d such that a ≤ d + b; this way we have ↑p - ↑q = ↑(p - q), ∞ - ↑p = ∞, ↑p - ∞ = ∞ - ∞ = 0; note that there is no negation, only subtraction;

The addition and multiplication defined this way together with 0 = ↑0 and 1 = ↑1 turn ℝ≥0∞ into a canonically ordered commutative semiring of characteristic zero.

• a⁻¹ is defined as Inf {b | 1 ≤ a * b}. This way we have (↑p)⁻¹ = ↑(p⁻¹) for p : ℝ≥0, p ≠ 0, 0⁻¹ = ∞, and ∞⁻¹ = 0.
• a / b is defined as a * b⁻¹.

This inversion and division include Inv and Div instances on ℝ≥0∞, making it into a DivInvOneMonoid. Further properties of these are shown in Data.ENNReal.Inv.

• Coercions to/from other types:

## Implementation notes #

We define a CanLift ℝ≥0∞ ℝ≥0 instance, so one of the ways to prove theorems about an ℝ≥0∞ number a is to consider the cases a = ∞ and a ≠ ∞, and use the tactic lift a to ℝ≥0 using ha in the second case. This instance is even more useful if one already has ha : a ≠ ∞ in the context, or if we have (f : α → ℝ≥0∞) (hf : ∀ x, f x ≠ ∞).

## Notations #

• ℝ≥0∞: the type of the extended nonnegative real numbers;
• ℝ≥0: the type of nonnegative real numbers [0, ∞); defined in Data.Real.NNReal;
• : a localized notation in ENNReal for ⊤ : ℝ≥0∞.

The extended nonnegative real numbers. This is usually denoted [0, ∞], and is relevant as the codomain of a measure.

Equations
Instances For

The extended nonnegative real numbers. This is usually denoted [0, ∞], and is relevant as the codomain of a measure.

Equations
Instances For

Notation for infinity as an ENNReal number.

Equations
Instances For
Equations
Equations
Equations
noncomputable instance ENNReal.instCompleteLinearOrder :
Equations
Equations
noncomputable instance ENNReal.instSub :
Equations
noncomputable instance ENNReal.instOrderedSub :
Equations
noncomputable instance ENNReal.instInv :
Equations
noncomputable instance ENNReal.instDivInvMonoid :
Equations
instance ENNReal.covariantClass_mul_le :
CovariantClass ENNReal ENNReal (fun (x x_1 : ENNReal) => x * x_1) fun (x x_1 : ENNReal) => x x_1
Equations
CovariantClass ENNReal ENNReal (fun (x x_1 : ENNReal) => x + x_1) fun (x x_1 : ENNReal) => x x_1
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
@[match_pattern]

Coercion from ℝ≥0 to ℝ≥0∞.

Equations
Instances For
def ENNReal.recTopCoe {C : ENNRealSort u_2} (top : C ) (coe : (x : NNReal) → C x) (x : ENNReal) :
C x

A version of WithTop.recTopCoe that uses ENNReal.ofNNReal.

Equations
Instances For
@[simp]
theorem ENNReal.none_eq_top :
none =
@[simp]
theorem ENNReal.some_eq_coe (a : NNReal) :
some a = a
@[simp]
theorem ENNReal.some_eq_coe' (a : NNReal) :
a = a
@[simp]
theorem ENNReal.coe_inj {p : NNReal} {q : NNReal} :
p = q p = q
theorem ENNReal.coe_ne_coe {p : NNReal} {q : NNReal} :
p q p q

toNNReal x returns x if it is real, otherwise 0.

Equations
Instances For

toReal x returns x if it is real, 0 otherwise.

Equations
• a.toReal = a.toNNReal
Instances For
noncomputable def ENNReal.ofReal (r : ) :

ofReal x returns x if it is nonnegative, 0 otherwise.

Equations
• = r.toNNReal
Instances For
@[simp]
theorem ENNReal.toNNReal_coe {r : NNReal} :
(r).toNNReal = r
@[simp]
theorem ENNReal.coe_toNNReal {a : ENNReal} :
a a.toNNReal = a
@[simp]
theorem ENNReal.ofReal_toReal {a : ENNReal} (h : a ) :
ENNReal.ofReal a.toReal = a
@[simp]
theorem ENNReal.toReal_ofReal {r : } (h : 0 r) :
().toReal = r
theorem ENNReal.toReal_ofReal' {r : } :
().toReal = max r 0
theorem ENNReal.coe_toNNReal_le_self {a : ENNReal} :
a.toNNReal a
theorem ENNReal.coe_nnreal_eq (r : NNReal) :
r =
theorem ENNReal.ofReal_eq_coe_nnreal {x : } (h : 0 x) :
= x, h
@[simp]
theorem ENNReal.ofReal_coe_nnreal {p : NNReal} :
= p
@[simp]
theorem ENNReal.coe_zero :
0 = 0
@[simp]
theorem ENNReal.coe_one :
1 = 1
@[simp]
theorem ENNReal.toReal_nonneg {a : ENNReal} :
0 a.toReal
@[simp]
theorem ENNReal.top_toNNReal :
.toNNReal = 0
@[simp]
theorem ENNReal.top_toReal :
.toReal = 0
@[simp]
@[simp]
@[simp]
theorem ENNReal.coe_toReal (r : NNReal) :
(r).toReal = r
@[simp]
@[simp]
@[simp]
@[simp]
theorem ENNReal.forall_ennreal {p : } :
(∀ (a : ENNReal), p a) (∀ (r : NNReal), p r) p
theorem ENNReal.forall_ne_top {p : } :
(∀ (a : ENNReal), a p a) ∀ (r : NNReal), p r
theorem ENNReal.exists_ne_top {p : } :
(∃ (a : ENNReal), a p a) ∃ (r : NNReal), p r
theorem ENNReal.toNNReal_eq_zero_iff (x : ENNReal) :
x.toNNReal = 0 x = 0 x =
theorem ENNReal.toReal_eq_zero_iff (x : ENNReal) :
x.toReal = 0 x = 0 x =
theorem ENNReal.toNNReal_ne_zero {a : ENNReal} :
a.toNNReal 0 a 0 a
theorem ENNReal.toReal_ne_zero {a : ENNReal} :
a.toReal 0 a 0 a
theorem ENNReal.toNNReal_eq_one_iff (x : ENNReal) :
x.toNNReal = 1 x = 1
theorem ENNReal.toReal_eq_one_iff (x : ENNReal) :
x.toReal = 1 x = 1
theorem ENNReal.toNNReal_ne_one {a : ENNReal} :
a.toNNReal 1 a 1
theorem ENNReal.toReal_ne_one {a : ENNReal} :
a.toReal 1 a 1
@[simp]
theorem ENNReal.coe_ne_top {r : NNReal} :
r
@[simp]
theorem ENNReal.top_ne_coe {r : NNReal} :
r
@[simp]
theorem ENNReal.coe_lt_top {r : NNReal} :
r <
@[simp]
theorem ENNReal.ofReal_ne_top {r : } :
@[simp]
theorem ENNReal.ofReal_lt_top {r : } :
@[simp]
theorem ENNReal.top_ne_ofReal {r : } :
@[simp]
theorem ENNReal.toReal_ofReal_eq_iff {a : } :
().toReal = a 0 a
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem ENNReal.coe_le_coe {r : NNReal} {q : NNReal} :
r q r q
@[simp]
theorem ENNReal.coe_lt_coe {r : NNReal} {q : NNReal} :
r < q r < q
theorem ENNReal.coe_le_coe_of_le {r : NNReal} {q : NNReal} :
r qr q

Alias of the reverse direction of ENNReal.coe_le_coe.

theorem ENNReal.coe_lt_coe_of_lt {r : NNReal} {q : NNReal} :
r < qr < q

Alias of the reverse direction of ENNReal.coe_lt_coe.

@[simp]
theorem ENNReal.coe_eq_zero {r : NNReal} :
r = 0 r = 0
@[simp]
theorem ENNReal.zero_eq_coe {r : NNReal} :
0 = r 0 = r
@[simp]
theorem ENNReal.coe_eq_one {r : NNReal} :
r = 1 r = 1
@[simp]
theorem ENNReal.one_eq_coe {r : NNReal} :
1 = r 1 = r
@[simp]
theorem ENNReal.coe_pos {r : NNReal} :
0 < r 0 < r
theorem ENNReal.coe_ne_zero {r : NNReal} :
r 0 r 0
theorem ENNReal.coe_ne_one {r : NNReal} :
r 1 r 1
@[simp]
theorem ENNReal.coe_add (x : NNReal) (y : NNReal) :
(x + y) = x + y
@[simp]
theorem ENNReal.coe_mul (x : NNReal) (y : NNReal) :
(x * y) = x * y
theorem ENNReal.coe_nsmul (n : ) (x : NNReal) :
(n x) = n x
@[simp]
theorem ENNReal.coe_pow (x : NNReal) (n : ) :
(x ^ n) = x ^ n
@[simp]
theorem ENNReal.coe_ofNat (n : ) [n.AtLeastTwo] :
() =
theorem ENNReal.coe_two :
2 = 2
theorem ENNReal.toNNReal_eq_toNNReal_iff (x : ENNReal) (y : ENNReal) :
x.toNNReal = y.toNNReal x = y x = 0 y = x = y = 0
theorem ENNReal.toReal_eq_toReal_iff (x : ENNReal) (y : ENNReal) :
x.toReal = y.toReal x = y x = 0 y = x = y = 0
theorem ENNReal.toNNReal_eq_toNNReal_iff' {x : ENNReal} {y : ENNReal} (hx : x ) (hy : y ) :
x.toNNReal = y.toNNReal x = y
theorem ENNReal.toReal_eq_toReal_iff' {x : ENNReal} {y : ENNReal} (hx : x ) (hy : y ) :
x.toReal = y.toReal x = y
@[simp]
@[simp]

(1 : ℝ≥0∞) ≤ 1, recorded as a Fact for use with Lp spaces.

Equations

(1 : ℝ≥0∞) ≤ 2, recorded as a Fact for use with Lp spaces.

Equations

(1 : ℝ≥0∞) ≤ ∞, recorded as a Fact for use with Lp spaces.

Equations

The set of numbers in ℝ≥0∞ that are not equal to is equivalent to ℝ≥0.

Equations
Instances For
theorem ENNReal.cinfi_ne_top {α : Type u_1} [] (f : ENNRealα) :
⨅ (x : { x : ENNReal // x }), f x = ⨅ (x : NNReal), f x
theorem ENNReal.iInf_ne_top {α : Type u_1} [] (f : ENNRealα) :
⨅ (x : ENNReal), ⨅ (_ : x ), f x = ⨅ (x : NNReal), f x
theorem ENNReal.csupr_ne_top {α : Type u_1} [] (f : ENNRealα) :
⨆ (x : { x : ENNReal // x }), f x = ⨆ (x : NNReal), f x
theorem ENNReal.iSup_ne_top {α : Type u_1} [] (f : ENNRealα) :
⨆ (x : ENNReal), ⨆ (_ : x ), f x = ⨆ (x : NNReal), f x
theorem ENNReal.iInf_ennreal {α : Type u_2} [] {f : ENNRealα} :
⨅ (n : ENNReal), f n = (⨅ (n : NNReal), f n) f
theorem ENNReal.iSup_ennreal {α : Type u_2} [] {f : ENNRealα} :
⨆ (n : ENNReal), f n = (⨆ (n : NNReal), f n) f

Coercion ℝ≥0 → ℝ≥0∞ as a RingHom.

Equations
Instances For
@[simp]
theorem ENNReal.coe_ofNNRealHom :
= some
@[simp]
theorem ENNReal.coe_indicator {α : Type u_2} (s : Set α) (f : αNNReal) (a : α) :
(s.indicator f a) = s.indicator (fun (x : α) => (f x)) a
@[simp]
theorem ENNReal.one_le_coe_iff {r : NNReal} :
1 r 1 r
@[simp]
theorem ENNReal.coe_le_one_iff {r : NNReal} :
r 1 r 1
@[simp]
theorem ENNReal.coe_lt_one_iff {p : NNReal} :
p < 1 p < 1
@[simp]
theorem ENNReal.one_lt_coe_iff {p : NNReal} :
1 < p 1 < p
@[simp]
theorem ENNReal.coe_natCast (n : ) :
n = n
@[simp]
theorem ENNReal.ofReal_natCast (n : ) :
= n
@[simp]
theorem ENNReal.ofReal_ofNat (n : ) [n.AtLeastTwo] :
@[simp]
theorem ENNReal.natCast_ne_top (n : ) :
n
@[simp]
theorem ENNReal.top_ne_natCast (n : ) :
n
@[simp]
@[simp]
theorem ENNReal.toNNReal_nat (n : ) :
(n).toNNReal = n
@[simp]
theorem ENNReal.toReal_nat (n : ) :
(n).toReal = n
@[simp]
theorem ENNReal.toReal_ofNat (n : ) [n.AtLeastTwo] :
().toReal =
theorem ENNReal.le_coe_iff {a : ENNReal} {r : NNReal} :
a r ∃ (p : NNReal), a = p p r
theorem ENNReal.coe_le_iff {a : ENNReal} {r : NNReal} :
r a ∀ (p : NNReal), a = pr p
theorem ENNReal.lt_iff_exists_coe {a : ENNReal} {b : ENNReal} :
a < b ∃ (p : NNReal), a = p p < b
theorem ENNReal.toReal_le_coe_of_le_coe {a : ENNReal} {b : NNReal} (h : a b) :
a.toReal b
@[simp]
theorem ENNReal.coe_finset_sup {α : Type u_1} {s : } {f : αNNReal} :
(s.sup f) = s.sup fun (x : α) => (f x)
@[simp]
theorem ENNReal.max_eq_zero_iff {a : ENNReal} {b : ENNReal} :
max a b = 0 a = 0 b = 0
@[simp]
theorem ENNReal.sup_eq_max {a : ENNReal} {b : ENNReal} :
a b = max a b
theorem ENNReal.lt_iff_exists_rat_btwn {a : ENNReal} {b : ENNReal} :
a < b ∃ (q : ), 0 q a < (q).toNNReal (q).toNNReal < b
theorem ENNReal.lt_iff_exists_real_btwn {a : ENNReal} {b : ENNReal} :
a < b ∃ (r : ), 0 r
theorem ENNReal.lt_iff_exists_nnreal_btwn {a : ENNReal} {b : ENNReal} :
a < b ∃ (r : NNReal), a < r r < b
theorem ENNReal.lt_iff_exists_add_pos_lt {a : ENNReal} {b : ENNReal} :
a < b ∃ (r : NNReal), 0 < r a + r < b
theorem ENNReal.le_of_forall_pos_le_add {a : ENNReal} {b : ENNReal} (h : ∀ (ε : NNReal), 0 < εb < a b + ε) :
a b
theorem ENNReal.natCast_lt_coe {r : NNReal} {n : } :
n < r n < r
theorem ENNReal.coe_lt_natCast {r : NNReal} {n : } :
r < n r < n
@[deprecated ENNReal.coe_natCast]
theorem ENNReal.coe_nat (n : ) :
n = n

Alias of ENNReal.coe_natCast.

@[deprecated ENNReal.ofReal_natCast]
theorem ENNReal.ofReal_coe_nat (n : ) :
= n

Alias of ENNReal.ofReal_natCast.

@[deprecated ENNReal.natCast_ne_top]
theorem ENNReal.nat_ne_top (n : ) :
n

Alias of ENNReal.natCast_ne_top.

@[deprecated ENNReal.top_ne_natCast]
theorem ENNReal.top_ne_nat (n : ) :
n

Alias of ENNReal.top_ne_natCast.

@[deprecated ENNReal.natCast_lt_coe]
theorem ENNReal.coe_nat_lt_coe {r : NNReal} {n : } :
n < r n < r

Alias of ENNReal.natCast_lt_coe.

@[deprecated ENNReal.coe_lt_natCast]
theorem ENNReal.coe_lt_coe_nat {r : NNReal} {n : } :
r < n r < n

Alias of ENNReal.coe_lt_natCast.

theorem ENNReal.exists_nat_gt {r : ENNReal} (h : r ) :
∃ (n : ), r < n
@[simp]
theorem ENNReal.iUnion_Iio_coe_nat :
⋃ (n : ), Set.Iio n = {}
@[simp]
theorem ENNReal.iUnion_Iic_coe_nat :
⋃ (n : ), Set.Iic n = {}
@[simp]
theorem ENNReal.iUnion_Ioc_coe_nat {a : ENNReal} :
⋃ (n : ), Set.Ioc a n = \ {}
@[simp]
theorem ENNReal.iUnion_Ioo_coe_nat {a : ENNReal} :
⋃ (n : ), Set.Ioo a n = \ {}
@[simp]
theorem ENNReal.iUnion_Icc_coe_nat {a : ENNReal} :
⋃ (n : ), Set.Icc a n = \ {}
@[simp]
theorem ENNReal.iUnion_Ico_coe_nat {a : ENNReal} :
⋃ (n : ), Set.Ico a n = \ {}
@[simp]
theorem ENNReal.iInter_Ici_coe_nat :
⋂ (n : ), Set.Ici n = {}
@[simp]
theorem ENNReal.iInter_Ioi_coe_nat :
⋂ (n : ), Set.Ioi n = {}
@[simp]
theorem ENNReal.coe_min (r : NNReal) (p : NNReal) :
(min r p) = min r p
@[simp]
theorem ENNReal.coe_max (r : NNReal) (p : NNReal) :
(max r p) = max r p
theorem ENNReal.le_of_top_imp_top_of_toNNReal_le {a : ENNReal} {b : ENNReal} (h : a = b = ) (h_nnreal : a b a.toNNReal b.toNNReal) :
a b
@[simp]
theorem ENNReal.abs_toReal {x : ENNReal} :
|x.toReal| = x.toReal
theorem ENNReal.coe_sSup {s : } :
(sSup s) = as, a
theorem ENNReal.coe_sInf {s : } (hs : s.Nonempty) :
(sInf s) = as, a
theorem ENNReal.coe_iSup {ι : Sort u_3} {f : ιNNReal} (hf : ) :
(iSup f) = ⨆ (a : ι), (f a)
theorem ENNReal.coe_iInf {ι : Sort u_3} [] (f : ιNNReal) :
(iInf f) = ⨅ (a : ι), (f a)
theorem ENNReal.coe_mem_upperBounds {r : NNReal} {s : } :
r r
theorem ENNReal.iSup_coe_eq_top {ι : Sort u_2} {f : ιNNReal} :
⨆ (i : ι), (f i) = ¬
theorem ENNReal.iSup_coe_lt_top {ι : Sort u_2} {f : ιNNReal} :
⨆ (i : ι), (f i) <
theorem ENNReal.iInf_coe_eq_top {ι : Sort u_2} {f : ιNNReal} :
⨅ (i : ι), (f i) =
theorem ENNReal.iInf_coe_lt_top {ι : Sort u_2} {f : ιNNReal} :
⨅ (i : ι), (f i) <
theorem Set.OrdConnected.preimage_coe_nnreal_ennreal {u : } (h : u.OrdConnected) :
().OrdConnected
theorem Set.OrdConnected.image_coe_nnreal_ennreal {t : } (h : t.OrdConnected) :
().OrdConnected
theorem Set.OrdConnected.preimage_ennreal_ofReal {u : } (h : u.OrdConnected) :
().OrdConnected
theorem Set.OrdConnected.image_ennreal_ofReal {s : } (h : s.OrdConnected) :
().OrdConnected

Extension for the positivity tactic: ENNReal.toReal.

Instances For

Extension for the positivity tactic: ENNReal.ofNNReal.

Instances For
@[deprecated le_inv_smul_iff_of_pos]
theorem ENNReal.le_inv_smul_iff_of_pos {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [] [] [] [] [] [] (ha : 0 < a) :
b₁ a⁻¹ b₂ a b₁ b₂

Alias of le_inv_smul_iff_of_pos.

@[deprecated inv_smul_le_iff_of_pos]
theorem ENNReal.inv_smul_le_iff_of_pos {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [] [] [] [] [] [] (ha : 0 < a) :
a⁻¹ b₁ b₂ b₁ a b₂

Alias of inv_smul_le_iff_of_pos.