data.real.ereal

# 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

@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
def ereal  :
Type

ereal : The type [-∞, ∞]

Equations
def real.to_ereal  :

The canonical inclusion froms reals to ereals. Do not use directly: as this is registered as a coercion, use the coercion instead.

Equations
@[simp]
theorem ereal.bot_lt_top  :
@[simp]
theorem ereal.bot_ne_top  :
@[instance]
Equations
@[simp]
theorem ereal.coe_le_coe_iff {x y : } :
x y x y
@[simp]
theorem ereal.coe_lt_coe_iff {x y : } :
x < y x < y
@[simp]
theorem ereal.coe_eq_coe_iff {x y : } :
x = y x = y

The canonical map from nonnegative extended reals to extended reals

Equations
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
theorem ereal.cases (a : ereal) :
a = (∃ (x : ), a = x) a =

A way to case on an element of ereal, separating the bot, real and top cases. A typical invocation looks like rcases x.cases with rfl|⟨x, rfl⟩|rfl

### Real coercion #

@[instance]
Equations
def ereal.to_real  :

The map from extended reals to reals sending infinities to zero.

Equations
@[simp]
theorem ereal.to_real_top  :
@[simp]
theorem ereal.to_real_bot  :
@[simp]
theorem ereal.to_real_zero  :
@[simp]
theorem ereal.to_real_coe (x : ) :
@[simp]
theorem ereal.bot_lt_coe (x : ) :
@[simp]
theorem ereal.coe_ne_bot (x : ) :
@[simp]
theorem ereal.bot_ne_coe (x : ) :
@[simp]
theorem ereal.coe_lt_top (x : ) :
@[simp]
theorem ereal.coe_ne_top (x : ) :
@[simp]
theorem ereal.top_ne_coe (x : ) :
@[simp]
theorem ereal.bot_lt_zero  :
< 0
@[simp]
theorem ereal.bot_ne_zero  :
@[simp]
theorem ereal.zero_ne_bot  :
@[simp]
theorem ereal.zero_lt_top  :
0 <
@[simp]
theorem ereal.zero_ne_top  :
@[simp]
theorem ereal.top_ne_zero  :
@[simp]
theorem ereal.coe_add (x y : ) :
(x + y) = x + y
@[simp]
theorem ereal.coe_zero  :
0 = 0
theorem ereal.to_real_le_to_real {x y : ereal} (h : x y) (hx : x ) (hy : y ) :
theorem ereal.coe_to_real {x : ereal} (hx : x ) (h'x : x ) :

### ennreal coercion #

@[simp]
theorem ereal.coe_ennreal_top  :
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem ereal.coe_ennreal_add (x y : ℝ≥0∞) :
(x + y) = x + y
@[simp]
theorem ereal.coe_ennreal_zero  :
0 = 0

### Order #

theorem ereal.exists_rat_btwn_of_lt {a b : ereal} (hab : a < b) :
∃ (x : ), a < x x < b
theorem ereal.lt_iff_exists_rat_btwn {a b : ereal} :
a < b ∃ (x : ), a < x x < b
theorem ereal.lt_iff_exists_real_btwn {a b : ereal} :
a < b ∃ (x : ), a < x x < b

The set of numbers in ereal that are not equal to ±∞ is equivalent to ℝ.

Equations

@[simp]
theorem ereal.add_top (x : ereal) :
@[simp]
theorem ereal.top_add (x : ereal) :
@[simp]
@[simp]
theorem ereal.bot_add_coe (x : ) :
@[simp]
theorem ereal.coe_add_bot (x : ) :
theorem ereal.to_real_add {x y : ereal} (hx : x ) (h'x : x ) (hy : y ) (h'y : y ) :
theorem ereal.add_lt_add_right_coe {x y : ereal} (h : x < y) (z : ) :
x + z < y + z
theorem ereal.add_lt_add_of_lt_of_le {x y z t : ereal} (h : x < y) (h' : z t) (hz : z ) (ht : t ) :
x + z < y + t
theorem ereal.add_lt_add_left_coe {x y : ereal} (h : x < y) (z : ) :
z + x < z + y
theorem ereal.add_lt_add {x y z t : ereal} (h1 : x < y) (h2 : z < t) :
x + z < y + t
@[simp]
theorem ereal.add_eq_top_iff {x y : ereal} :
x + y = x = y =
@[simp]
theorem ereal.add_lt_top_iff {x y : ereal} :
x + y < x < y <

### Negation #

def ereal.neg  :

negation on ereal

Equations
@[instance]
Equations
theorem ereal.neg_def (x : ) :
@[simp]
theorem ereal.neg_top  :
@[simp]
theorem ereal.neg_bot  :
@[simp]
theorem ereal.neg_zero  :
-0 = 0
@[simp]
theorem ereal.neg_neg (a : ereal) :
--a = a

- -a = a on ereal.

theorem ereal.neg_inj {a b : ereal} (h : -a = -b) :
a = b
@[simp]
theorem ereal.neg_eq_neg_iff (a b : ereal) :
-a = -b a = b
@[simp]
theorem ereal.to_real_neg {a : ereal} :
theorem ereal.neg_eq_iff_neg_eq {a b : ereal} :
-a = b -b = a

Even though ereal is not an additive group, -a = b ↔ -b = a still holds

@[simp]
theorem ereal.neg_eg_top_iff {x : ereal} :
-x = x =
@[simp]
theorem ereal.neg_eg_bot_iff {x : ereal} :
-x = x =
@[simp]
theorem ereal.neg_eg_zero_iff {x : ereal} :
-x = 0 x = 0
theorem ereal.neg_le_of_neg_le {a b : ereal} (h : -a b) :
-b a

if -a ≤ b then -b ≤ a on ereal.

theorem ereal.neg_le {a b : ereal} :
-a b -b a

-a ≤ b ↔ -b ≤ a on ereal.

theorem ereal.le_neg_of_le_neg {a b : ereal} (h : a -b) :
b -a

a ≤ -b → b ≤ -a on ereal

@[simp]
theorem ereal.neg_le_neg_iff {a b : ereal} :
-a -b b a
@[simp]
theorem ereal.coe_neg (x : ) :

Negation as an order reversing isomorphism on ereal.

Equations
theorem ereal.neg_lt_of_neg_lt {a b : ereal} (h : -a < b) :
-b < a
theorem ereal.neg_lt_iff_neg_lt {a b : ereal} :
-a < b -b < a

### Subtraction #

def ereal.sub (x y : ereal) :

Subtraction on ereal, defined by x - y = x + (-y). Since addition is badly behaved at some points, so is subtraction. There is no standard algebraic typeclass involving subtraction that is registered on ereal because of this bad behavior.

Equations
@[instance]
Equations
@[simp]
theorem ereal.top_sub (x : ereal) :
@[simp]
theorem ereal.sub_bot (x : ereal) :
@[simp]
theorem ereal.bot_sub_top  :
@[simp]
theorem ereal.bot_sub_coe (x : ) :
@[simp]
theorem ereal.coe_sub_bot (x : ) :
@[simp]
theorem ereal.sub_zero (x : ereal) :
x - 0 = x
@[simp]
theorem ereal.zero_sub (x : ereal) :
0 - x = -x
theorem ereal.sub_eq_add_neg (x y : ereal) :
x - y = x + -y
theorem ereal.sub_le_sub {x y z t : ereal} (h : x y) (h' : t z) :
x - z y - t
theorem ereal.sub_lt_sub_of_lt_of_le {x y z t : ereal} (h : x < y) (h' : z t) (hz : z ) (ht : t ) :
x - t < y - z
theorem ereal.to_real_sub {x y : ereal} (hx : x ) (h'x : x ) (hy : y ) (h'y : y ) :

### Multiplication #

@[simp]
theorem ereal.coe_one  :
1 = 1
@[simp]
theorem ereal.coe_mul (x y : ) :
x * y = (x) * y
@[simp]
theorem ereal.mul_top (x : ereal) (h : x 0) :
@[simp]
theorem ereal.top_mul (x : ereal) (h : x 0) :
@[simp]
theorem ereal.bot_mul_bot  :
@[simp]
theorem ereal.bot_mul_coe (x : ) (h : x 0) :
@[simp]
theorem ereal.coe_mul_bot (x : ) (h : x 0) :
@[simp]
theorem ereal.to_real_one  :
theorem ereal.to_real_mul {x y : ereal} :
(x * y).to_real = (x.to_real) * y.to_real