Extended non-negative reals
We define ennreal := with_no ℝ≥0
to be the type of extended nonnegative real numbers, i.e., the
interval [0, +∞]
. This type is used as the codomain of a measure_theory.measure
, and of the
extended distance edist
in a emetric_space
. In this file we define some algebraic operations and
a linear order on ennreal
and prove basic properties of these operations, order, and conversions
to/from ℝ
, ℝ≥0
, and ℕ
.
Main definitions
ennreal
: the extended nonnegative real numbers[0, ∞]
; defined aswith_top ℝ≥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)
anda + ∞ = ∞ + a = ∞
;a * b
is defined so that↑p * ↑q = ↑(p * q)
for(p q : ℝ≥0)
,0 * ∞ = ∞ * 0 = 0
, anda * ∞ = ∞ * a = ∞
fora ≠ 0
;a - b
is defined as the minimald
such thata ≤ d + b
; this way we have↑p - ↑q = ↑(p - q)
,∞ - ↑p = ∞
,↑p - ∞ = ∞ - ∞ = 0
; note that there is no negation, only subtraction;a⁻¹
is defined asInf {b | 1 ≤ a * b}
. This way we have(↑p)⁻¹ = ↑(p⁻¹)
forp : ℝ≥0
,p ≠ 0
,0⁻¹ = ∞
, and∞⁻¹ = 0
.a / b
is defined asa * b⁻¹
.
The addition and multiplication defined this way together with
0 = ↑0
and1 = ↑1
turnennreal
into a canonically ordered commutative semiring of characteristic zero.Coercions to/from other types:
coercion
ℝ≥0 → ennreal
is defined ashas_coe
, so one can use(p : ℝ≥0)
in a context that expectsa : ennreal
, and Lean will applycoe
automatically;ennreal.to_nnreal
sends↑p
top
and∞
to0
;ennreal.to_real := coe ∘ ennreal.to_nnreal
sends↑p
,p : ℝ≥0
to(↑p : ℝ)
and∞
to0
;ennreal.of_real := coe ∘ nnreal.of_real
sendsx : ℝ
to↑⟨max x 0, _⟩
ennreal.ne_top_equiv_nnreal
is an equivalence between{a : ennreal // a ≠ 0}
andℝ≥0
.
Implementation notes
We define a can_lift ennreal ℝ≥0
instance, so one of the ways to prove theorems about an ennreal
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 : α → ennreal) (hf : ∀ x, f x ≠ ∞)
.
Notations
Equations
- ennreal.inhabited = {default := 0}
to_nnreal x
returns x
if it is real, otherwise 0.
Equations
- ennreal.to_nnreal (some r) = r
- ennreal.to_nnreal none = 0
of_real x
returns x
if it is nonnegative, 0
otherwise.
Equations
- ennreal.of_real r = ↑(nnreal.of_real r)
The set of ennreal
numbers that are not equal to ∞
is equivalent to ℝ≥0
.
Coercion ℝ≥0 → ennreal
as a ring_hom
.
Equations
- ennreal.of_nnreal_hom = {to_fun := coe coe_to_lift, map_one' := ennreal.coe_one, map_mul' := ennreal.of_nnreal_hom._proof_1, map_zero' := ennreal.coe_zero, map_add' := ennreal.of_nnreal_hom._proof_2}
Equations
- ennreal.div_inv_monoid = {mul := monoid.mul infer_instance, mul_assoc := ennreal.div_inv_monoid._proof_1, one := monoid.one infer_instance, one_mul := ennreal.div_inv_monoid._proof_2, mul_one := ennreal.div_inv_monoid._proof_3, inv := has_inv.inv ennreal.has_inv, div := λ (a b : ennreal), monoid.mul a b⁻¹, div_eq_mul_inv := ennreal.div_inv_monoid._proof_4}
ennreal.to_nnreal
as a monoid_hom
.
Equations
- ennreal.to_nnreal_hom = {to_fun := ennreal.to_nnreal, map_one' := ennreal.to_nnreal_hom._proof_1, map_mul' := ennreal.to_nnreal_hom._proof_2}
ennreal.to_real
as a monoid_hom
.
supr_mul
, mul_supr
and variants are in topology.instances.ennreal
.
le_of_add_le_add_left
is normally applicable to ordered_cancel_add_comm_monoid
,
but it holds in ennreal
with the additional assumption that a < ∞
.