mathlib documentation

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

@[protected, instance]
@[protected, instance]
noncomputable def ereal.has_Sup  :
@[protected, instance]
noncomputable def ereal.has_Inf  :
@[protected, instance]
@[protected, instance]
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
@[protected, instance]
Equations
@[simp]
theorem ereal.bot_lt_top  :
@[simp]
theorem ereal.bot_ne_top  :
@[protected, instance]
Equations
@[protected, simp, norm_cast]
theorem ereal.coe_le_coe_iff {x y : } :
x y x y
@[protected, simp, norm_cast]
theorem ereal.coe_lt_coe_iff {x y : } :
x < y x < y
@[protected, simp, norm_cast]
theorem ereal.coe_eq_coe_iff {x y : } :
x = y x = y

The canonical map from nonnegative extended reals to extended reals

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected]
def ereal.rec {C : erealSort u_1} (h_bot : C ) (h_real : Π (a : ), C a) (h_top : C ) (a : ereal) :
C a

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.

Equations

Real coercion #

@[protected, 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, norm_cast]
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 ) :
theorem ereal.le_coe_to_real {x : ereal} (h : x ) :
theorem ereal.coe_to_real_le {x : ereal} (h : x ) :
theorem ereal.eq_top_iff_forall_lt (x : ereal) :
x = ∀ (y : ), y < x
theorem ereal.eq_bot_iff_forall_lt (x : ereal) :
x = ∀ (y : ), x < y

ennreal coercion #

@[simp]
@[simp]
@[simp]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp]
@[simp]
@[simp, norm_cast]
theorem ereal.coe_ennreal_add (x y : ennreal) :
(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

Addition #

@[simp]
theorem ereal.add_top (x : ereal) :
@[simp]
theorem ereal.top_add (x : ereal) :
@[simp]
theorem ereal.bot_add_bot  :
@[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 #

@[protected]
def ereal.neg  :

negation on ereal

Equations
@[protected, instance]
Equations
@[protected, norm_cast]
theorem ereal.neg_def (x : ) :
@[simp]
theorem ereal.neg_top  :
@[simp]
theorem ereal.neg_bot  :
@[simp]
theorem ereal.neg_zero  :
-0 = 0
@[protected, instance]
Equations
@[simp]
theorem ereal.to_real_neg {a : ereal} :
@[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
@[protected]
theorem ereal.neg_le_of_neg_le {a b : ereal} (h : -a b) :
-b a

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

@[protected]
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, norm_cast]
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 #

@[protected]
noncomputable 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
@[protected, instance]
noncomputable def ereal.has_sub  :
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, norm_cast]
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} :