Extended non-negative reals #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We define ennreal = ℝ≥0∞ := with_top ℝ≥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 ℝ≥0∞
and prove basic properties of these operations, order, and conversions to/from ℝ
, ℝ≥0
, and ℕ
.
Main definitions #
-
ℝ≥0∞
: 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
turnℝ≥0∞
into a canonically ordered commutative semiring of characteristic zero. -
-
Coercions to/from other types:
-
coercion
ℝ≥0 → ℝ≥0∞
is defined ashas_coe
, so one can use(p : ℝ≥0)
in a context that expectsa : ℝ≥0∞
, 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 ∘ real.to_nnreal
sendsx : ℝ
to↑⟨max x 0, _⟩
-
ennreal.ne_top_equiv_nnreal
is an equivalence between{a : ℝ≥0∞ // a ≠ 0}
andℝ≥0
.
-
Implementation notes #
We define a can_lift ℝ≥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 indata.real.nnreal
;∞
: a localized notation inℝ≥0∞
for⊤ : ℝ≥0∞
.
The extended nonnegative real numbers. This is usually denoted [0, ∞], and is relevant as the codomain of a measure.
Instances for ennreal
- ennreal.has_zero
- ennreal.add_comm_monoid_with_one
- ennreal.semilattice_sup
- ennreal.distrib_lattice
- ennreal.order_bot
- ennreal.bounded_order
- ennreal.canonically_ordered_comm_semiring
- ennreal.complete_linear_order
- ennreal.densely_ordered
- ennreal.nontrivial
- ennreal.canonically_linear_ordered_add_monoid
- ennreal.has_sub
- ennreal.has_ordered_sub
- ennreal.linear_ordered_add_comm_monoid_with_top
- ennreal.char_zero
- ennreal.covariant_class_mul_le
- ennreal.covariant_class_add_le
- ennreal.linear_ordered_comm_monoid_with_zero
- ennreal.inhabited
- ennreal.has_coe
- ennreal.can_lift
- ennreal.contravariant_class_add_lt
- ennreal.has_inv
- ennreal.div_inv_monoid
- ennreal.div_inv_one_monoid
- ennreal.has_involutive_inv
- ennreal.topological_space
- ennreal.order_topology
- ennreal.t2_space
- ennreal.normal_space
- ennreal.topological_space.second_countable_topology
- ennreal.has_continuous_add
- ennreal.has_continuous_inv
- ereal.has_coe_ennreal
- ennreal.measurable_space
- ennreal.borel_space
- ennreal.has_measurable_mul₂
- ennreal.has_measurable_sub₂
- ennreal.has_measurable_inv
- ennreal.real.has_pow
- topological_space.ennreal.metrizable_space
- ennreal.has_measurable_pow
- pmf.fun_like
- enat.has_coe_ennreal
Equations
- ennreal.linear_ordered_comm_monoid_with_zero = {le := linear_ordered_add_comm_monoid_with_top.le ennreal.linear_ordered_add_comm_monoid_with_top, lt := linear_ordered_add_comm_monoid_with_top.lt ennreal.linear_ordered_add_comm_monoid_with_top, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_ordered_add_comm_monoid_with_top.decidable_le ennreal.linear_ordered_add_comm_monoid_with_top, decidable_eq := linear_ordered_add_comm_monoid_with_top.decidable_eq ennreal.linear_ordered_add_comm_monoid_with_top, decidable_lt := linear_ordered_add_comm_monoid_with_top.decidable_lt ennreal.linear_ordered_add_comm_monoid_with_top, max := linear_ordered_add_comm_monoid_with_top.max ennreal.linear_ordered_add_comm_monoid_with_top, max_def := _, min := linear_ordered_add_comm_monoid_with_top.min ennreal.linear_ordered_add_comm_monoid_with_top, min_def := _, mul := comm_semiring.mul (show comm_semiring ennreal, from infer_instance), mul_assoc := ennreal.linear_ordered_comm_monoid_with_zero._proof_1, one := comm_semiring.one (show comm_semiring ennreal, from infer_instance), one_mul := ennreal.linear_ordered_comm_monoid_with_zero._proof_2, mul_one := ennreal.linear_ordered_comm_monoid_with_zero._proof_3, npow := comm_semiring.npow (show comm_semiring ennreal, from infer_instance), npow_zero' := ennreal.linear_ordered_comm_monoid_with_zero._proof_4, npow_succ' := ennreal.linear_ordered_comm_monoid_with_zero._proof_5, mul_comm := ennreal.linear_ordered_comm_monoid_with_zero._proof_6, mul_le_mul_left := ennreal.linear_ordered_comm_monoid_with_zero._proof_7, zero := linear_ordered_add_comm_monoid_with_top.zero ennreal.linear_ordered_add_comm_monoid_with_top, zero_mul := ennreal.linear_ordered_comm_monoid_with_zero._proof_8, mul_zero := ennreal.linear_ordered_comm_monoid_with_zero._proof_9, zero_le_one := ennreal.linear_ordered_comm_monoid_with_zero._proof_10}
Equations
- ennreal.add_units.unique = {to_inhabited := {default := 0}, uniq := ennreal.add_units.unique._proof_1}
Equations
- ennreal.inhabited = {default := 0}
Equations
to_nnreal x
returns x
if it is real, otherwise 0.
Equations
of_real x
returns x
if it is nonnegative, 0
otherwise.
Equations
- ennreal.of_real r = ↑(r.to_nnreal)
(1 : ℝ≥0∞) ≤ 1
, recorded as a fact
for use with Lp
spaces.
(1 : ℝ≥0∞) ≤ 2
, recorded as a fact
for use with Lp
spaces.
The set of numbers in ℝ≥0∞
that are not equal to ∞
is equivalent to ℝ≥0
.
Coercion ℝ≥0 → ℝ≥0∞
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}
A mul_action
over ℝ≥0∞
restricts to a mul_action
over ℝ≥0
.
A distrib_mul_action
over ℝ≥0∞
restricts to a distrib_mul_action
over ℝ≥0
.
A module
over ℝ≥0∞
restricts to a module
over ℝ≥0
.
Equations
An algebra
over ℝ≥0∞
restricts to an algebra
over ℝ≥0
.
Equations
- ennreal.algebra = {to_has_smul := {smul := has_smul.smul smul_zero_class.to_has_smul}, to_ring_hom := (algebra_map ennreal A).comp ennreal.of_nnreal_hom, commutes' := _, smul_def' := _}
An element a
is add_le_cancellable
if a + b ≤ a + c
implies b ≤ c
for all b
and c
.
This is true in ℝ≥0∞
for all elements except ∞
.
This lemma has an abbreviated name because it is used frequently.
This lemma has an abbreviated name because it is used frequently.
This lemma has an abbreviated name because it is used frequently.
This lemma has an abbreviated name because it is used frequently.
This is a special case of with_top.top_sub_coe
in the ennreal
namespace
This is a special case of with_top.sub_top
in the ennreal
namespace
Equations
- ennreal.has_inv = {inv := λ (a : ennreal), has_Inf.Inf {b : ennreal | 1 ≤ a * b}}
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, npow := monoid.npow infer_instance, npow_zero' := ennreal.div_inv_monoid._proof_4, npow_succ' := ennreal.div_inv_monoid._proof_5, inv := has_inv.inv ennreal.has_inv, div := λ (a b : ennreal), monoid.mul a b⁻¹, div_eq_mul_inv := ennreal.div_inv_monoid._proof_6, zpow := zpow_rec {inv := has_inv.inv ennreal.has_inv}, zpow_zero' := ennreal.div_inv_monoid._proof_12, zpow_succ' := ennreal.div_inv_monoid._proof_13, zpow_neg' := ennreal.div_inv_monoid._proof_14}
Equations
- ennreal.div_inv_one_monoid = {mul := div_inv_monoid.mul ennreal.div_inv_monoid, mul_assoc := _, one := div_inv_monoid.one ennreal.div_inv_monoid, one_mul := _, mul_one := _, npow := div_inv_monoid.npow ennreal.div_inv_monoid, npow_zero' := _, npow_succ' := _, inv := div_inv_monoid.inv ennreal.div_inv_monoid, div := div_inv_monoid.div ennreal.div_inv_monoid, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow ennreal.div_inv_monoid, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, inv_one := ennreal.div_inv_one_monoid._proof_1}
Equations
- ennreal.has_involutive_inv = {inv := has_inv.inv ennreal.has_inv, inv_inv := ennreal.has_involutive_inv._proof_1}
The inverse map λ x, x⁻¹
is an order isomorphism between ℝ≥0∞
and its order_dual
Equations
- order_iso.inv_ennreal = {to_equiv := equiv.trans (equiv.inv ennreal) order_dual.to_dual, map_rel_iff' := order_iso.inv_ennreal._proof_1}
The birational order isomorphism between ℝ≥0∞
and the unit interval set.Iic (1 : ℝ≥0∞)
.
Order isomorphism between an initial interval in ℝ≥0∞
and an initial interval in ℝ≥0
.
An order isomorphism between the extended nonnegative real numbers and the unit interval.
Alias of the reverse direction of ennreal.of_real_eq_zero
.
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
.
If x ≠ ∞
, then right multiplication by x
maps infimum over a nonempty type to infimum. See
also ennreal.infi_mul_of_ne
that assumes x ≠ 0
but does not require [nonempty ι]
.
If x ≠ ∞
, then left multiplication by x
maps infimum over a nonempty type to infimum. See
also ennreal.mul_infi_of_ne
that assumes x ≠ 0
but does not require [nonempty ι]
.
supr_mul
, mul_supr
and variants are in topology.instances.ennreal
.