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 asWithTop ℝ≥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;
The addition and multiplication defined this way together with
0 = ↑0
and1 = ↑1
turnℝ≥0∞
into a canonically ordered commutative semiring of characteristic zero.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⁻¹
.
This inversion and division include
Inv
andDiv
instances onℝ≥0∞
, making it into aDivInvOneMonoid
. Further properties of these are shown inData.ENNReal.Inv
.Coercions to/from other types:
coercion
ℝ≥0 → ℝ≥0∞
is defined asCoe
, so one can use(p : ℝ≥0)
in a context that expectsa : ℝ≥0∞
, and Lean will applycoe
automatically;ENNReal.toNNReal
sends↑p
top
and∞
to0
;ENNReal.toReal := coe ∘ ENNReal.toNNReal
sends↑p
,p : ℝ≥0
to(↑p : ℝ)
and∞
to0
;ENNReal.ofReal := coe ∘ Real.toNNReal
sendsx : ℝ
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 #
The extended nonnegative real numbers. This is usually denoted [0, ∞], and is relevant as the codomain of a measure.
Equations
- ENNReal.«termℝ≥0∞» = Lean.ParserDescr.node `ENNReal.termℝ≥0∞ 1024 (Lean.ParserDescr.symbol "ℝ≥0∞")
Instances For
Notation for infinity as an ENNReal
number.
Equations
- ENNReal.«term∞» = Lean.ParserDescr.node `ENNReal.term∞ 1024 (Lean.ParserDescr.symbol "∞")
Instances For
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
- One or more equations did not get rendered due to their size.
Equations
- ENNReal.instUniqueAddUnits = { default := 0, uniq := ENNReal.instUniqueAddUnits.proof_1 }
Equations
- ENNReal.instInhabited = { default := 0 }
Equations
- ENNReal.instCoeNNReal = { coe := ENNReal.ofNNReal }
A version of WithTop.recTopCoe
that uses ENNReal.ofNNReal
.
Equations
- ENNReal.recTopCoe top coe x = WithTop.recTopCoe top coe x
Instances For
Equations
ofReal x
returns x
if it is nonnegative, 0
otherwise.
Equations
- ENNReal.ofReal r = ↑r.toNNReal
Instances For
Alias of the reverse direction of ENNReal.coe_le_coe
.
Alias of the reverse direction of ENNReal.coe_lt_coe
.
(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
Coercion ℝ≥0 → ℝ≥0∞
as a RingHom
.
Equations
- ENNReal.ofNNRealHom = { toFun := some, map_one' := ENNReal.coe_one, map_mul' := ⋯, map_zero' := ENNReal.coe_zero, map_add' := ⋯ }
Instances For
Alias of ENNReal.coe_natCast
.
Alias of ENNReal.ofReal_natCast
.
Alias of ENNReal.natCast_ne_top
.
Alias of ENNReal.top_ne_natCast
.
Alias of ENNReal.natCast_lt_coe
.
Alias of ENNReal.coe_lt_natCast
.
Extension for the positivity
tactic: ENNReal.toReal
.
Instances For
Extension for the positivity
tactic: ENNReal.ofNNReal
.
Instances For
Alias of le_inv_smul_iff_of_pos
.
Alias of inv_smul_le_iff_of_pos
.