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

• coercion ℝ≥0 → ℝ≥0∞ is defined as Coe, so one can use (p : ℝ≥0) in a context that expects a : ℝ≥0∞, and Lean will apply coe automatically;

• ENNReal.toNNReal sends ↑p to p and ∞ to 0;

• ENNReal.toReal := coe ∘ ENNReal.toNNReal sends ↑p, p : ℝ≥0 to (↑p : ℝ) and ∞ to 0;

• ENNReal.ofReal := coe ∘ Real.toNNReal sends x : ℝ to ↑⟨max x 0, _⟩

• ENNReal.neTopEquivNNReal is an equivalence between {a : ℝ≥0∞ // a ≠ 0} and ℝ≥0.

## 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
noncomputable instance ENNReal.instSub :
Equations
Equations
• One or more equations did not get rendered due to their size.
noncomputable instance ENNReal.instInvENNReal :
Equations
noncomputable instance ENNReal.instDivInvMonoidENNReal :
Equations
• One or more equations did not get rendered due to their size.
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
• One or more equations did not get rendered due to their size.
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
• = ()
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) :
= { val := x, property := 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]
theorem ENNReal.one_toReal :
1.toReal = 1
@[simp]
theorem ENNReal.one_toNNReal :
1.toNNReal = 1
@[simp]
theorem ENNReal.coe_toReal (r : NNReal) :
(r).toReal = r
@[simp]
theorem ENNReal.zero_toNNReal :
0.toNNReal = 0
@[simp]
theorem ENNReal.zero_toReal :
0.toReal = 0
@[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
@[deprecated]
theorem ENNReal.exists_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 : ) [] :
() =
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
• One or more equations did not get rendered due to their size.
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 : α) :
() = Set.indicator s (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 : ) [] :
@[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 : ) [] :
().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} :
() = Finset.sup s 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 < () () < 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) = ⨆ a ∈ s, a
theorem ENNReal.coe_sInf {s : } :
(sInf s) = ⨅ a ∈ s, 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) <

Extension for the positivity tactic: ENNReal.toReal.

Instances For

Extension for the positivity tactic: ENNReal.ofNNReal.

Instances For

### Deprecated lemmas #

Those lemmas have been deprecated on the 2023/12/23.

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