The extended reals [-∞, ∞]. #
This file defines ereal
, the real numbers together with a top and bottom element,
referred to as ⊤ and ⊥. It is implemented as with_top (with_bot ℝ)
Addition and multiplication are problematic in the presence of ±∞, but negation has a natural definition and satisfies the usual properties.
An ad hoc addition is defined, for which ereal
is an add_comm_monoid
, and even an ordered one
(if a ≤ a'
and b ≤ b'
then a + b ≤ a' + b'
).
Note however that addition is badly behaved at (⊥, ⊤)
and (⊤, ⊥)
so this can not be upgraded
to a group structure. Our choice is that ⊥ + ⊤ = ⊤ + ⊥ = ⊤
.
An ad hoc subtraction is then defined by x - y = x + (-y)
. It does not have nice properties,
but it is sometimes convenient to have.
An ad hoc multiplication is defined, for which ereal
is a comm_monoid_with_zero
.
This does not distribute with addition, as ⊤ = ⊤ - ⊥ = 1*⊤ - 1*⊤ ≠ (1 - 1) * ⊤ = 0 * ⊤ = 0
.
ereal
is a complete_linear_order
; this is deduced by type class inference from
the fact that with_top (with_bot L)
is a complete linear order if L
is
a conditionally complete linear order.
Coercions from ℝ
and from ℝ≥0∞
are registered, and their basic properties are proved. The main
one is the real coercion, and is usually referred to just as coe
(lemmas such as
ereal.coe_add
deal with this coercion). The one from ennreal
is usually called coe_ennreal
in the ereal
namespace.
Tags #
real, ereal, complete lattice
TODO #
abs : ereal → ℝ≥0∞
In Isabelle they define + - * and / (making junk choices for things like -∞ + ∞) and then prove whatever bits of the ordered ring/field axioms still hold. They also do some limits stuff (liminf/limsup etc). See https://isabelle.in.tum.de/dist/library/HOL/HOL-Library/Extended_Real.html
ereal : The type [-∞, ∞]
Instances for ereal
- ereal.has_top
- ereal.comm_monoid_with_zero
- ereal.has_Sup
- ereal.has_Inf
- ereal.complete_linear_order
- ereal.linear_ordered_add_comm_monoid_with_top
- ereal.has_bot
- ereal.has_coe
- ereal.has_coe_ennreal
- ereal.has_zero
- ereal.inhabited
- ereal.real.can_lift
- ereal.has_neg
- ereal.has_involutive_neg
- ereal.has_sub
- ereal.topological_space
- ereal.order_topology
- ereal.t2_space
- ereal.topological_space.second_countable_topology
- ereal.measurable_space
- ereal.borel_space
The canonical inclusion froms reals to ereals. Do not use directly: as this is registered as a coercion, use the coercion instead.
Equations
Equations
- ereal.has_bot = {bot := option.some ⊥}
Equations
The canonical map from nonnegative extended reals to extended reals
Equations
- ennreal.to_ereal (option.some x) = ↑(x.val)
- ⊤.to_ereal = ⊤
Equations
Equations
- ereal.has_zero = {zero := ↑0}
Equations
- ereal.inhabited = {default := 0}
A recursor for ereal
in terms of the coercion.
A typical invocation looks like induction x using ereal.rec
. Note that using induction
directly will unfold ereal
to option
which is undesirable.
When working in term mode, note that pattern matching can be used directly.
Real coercion #
ennreal coercion #
Order #
The set of numbers in ereal
that are not equal to ±∞
is equivalent to ℝ
.
Addition #
Negation #
Equations
- ereal.has_neg = {neg := ereal.neg}
Equations
- ereal.has_involutive_neg = {neg := has_neg.neg ereal.has_neg, neg_neg := ereal.has_involutive_neg._proof_1}
Negation as an order reversing isomorphism on ereal
.
Equations
- ereal.neg_order_iso = {to_equiv := {to_fun := λ (x : ereal), ⇑order_dual.to_dual (-x), inv_fun := λ (x : erealᵒᵈ), -⇑order_dual.of_dual x, left_inv := ereal.neg_order_iso._proof_1, right_inv := ereal.neg_order_iso._proof_2}, map_rel_iff' := ereal.neg_order_iso._proof_3}
Subtraction #
Equations
- ereal.has_sub = {sub := ereal.sub}