mathlib documentation

data.real.hyperreal

Construction of the hyperreal numbers as an ultraproduct of real sequences. #

def hyperreal  :
Type

Hyperreal numbers on the ultrafilter extending the cofinite filter

Equations
@[instance]
Equations
@[simp]
theorem hyperreal.coe_eq_coe {x y : } :
x = y x = y
@[simp]
theorem hyperreal.coe_eq_zero {x : } :
x = 0 x = 0
@[simp]
theorem hyperreal.coe_eq_one {x : } :
x = 1 x = 1
@[simp]
theorem hyperreal.coe_one  :
1 = 1
@[simp]
theorem hyperreal.coe_zero  :
0 = 0
@[simp]
theorem hyperreal.coe_inv (x : ) :
@[simp]
theorem hyperreal.coe_neg (x : ) :
@[simp]
theorem hyperreal.coe_add (x y : ) :
(x + y) = x + y
@[simp]
theorem hyperreal.coe_bit0 (x : ) :
@[simp]
theorem hyperreal.coe_bit1 (x : ) :
@[simp]
theorem hyperreal.coe_mul (x y : ) :
x * y = (x) * y
@[simp]
theorem hyperreal.coe_div (x y : ) :
(x / y) = x / y
@[simp]
theorem hyperreal.coe_sub (x y : ) :
(x - y) = x - y
@[simp]
theorem hyperreal.coe_lt_coe {x y : } :
x < y x < y
@[simp]
theorem hyperreal.coe_pos {x : } :
0 < x 0 < x
@[simp]
theorem hyperreal.coe_le_coe {x y : } :
x y x y
@[simp]
theorem hyperreal.coe_abs (x : ) :
@[simp]
theorem hyperreal.coe_max (x y : ) :
(max x y) = max x y
@[simp]
theorem hyperreal.coe_min (x y : ) :
(min x y) = min x y
def hyperreal.of_seq (f : ) :

Construct a hyperreal number from a sequence of real numbers.

Equations

A sample infinitesimal hyperreal

Equations

A sample infinite hyperreal

Equations
theorem hyperreal.omega_pos  :
0 < ω
def hyperreal.is_st (x : ℝ*) (r : ) :
Prop

Standard part predicate

Equations
def hyperreal.st  :
ℝ*

Standard part function: like a "round" to ℝ instead of ℤ

Equations
def hyperreal.infinitesimal (x : ℝ*) :
Prop

A hyperreal number is infinitesimal if its standard part is 0

Equations
def hyperreal.infinite_pos (x : ℝ*) :
Prop

A hyperreal number is positive infinite if it is larger than all real numbers

Equations
def hyperreal.infinite_neg (x : ℝ*) :
Prop

A hyperreal number is negative infinite if it is smaller than all real numbers

Equations
def hyperreal.infinite (x : ℝ*) :
Prop

A hyperreal number is infinite if it is infinite positive or infinite negative

Equations

Some facts about st #

theorem hyperreal.is_st_unique {x : ℝ*} {r s : } (hr : x.is_st r) (hs : x.is_st s) :
r = s
theorem hyperreal.not_infinite_of_exists_st {x : ℝ*} :
(∃ (r : ), x.is_st r)¬x.infinite
theorem hyperreal.is_st_Sup {x : ℝ*} (hni : ¬x.infinite) :
x.is_st (Sup {y : | y < x})
theorem hyperreal.exists_st_of_not_infinite {x : ℝ*} (hni : ¬x.infinite) :
∃ (r : ), x.is_st r
theorem hyperreal.st_eq_Sup {x : ℝ*} :
x.st = Sup {y : | y < x}
theorem hyperreal.st_infinite {x : ℝ*} (hi : x.infinite) :
x.st = 0
theorem hyperreal.st_of_is_st {x : ℝ*} {r : } (hxr : x.is_st r) :
x.st = r
theorem hyperreal.is_st_st_of_is_st {x : ℝ*} {r : } (hxr : x.is_st r) :
x.is_st x.st
theorem hyperreal.is_st_st_of_exists_st {x : ℝ*} (hx : ∃ (r : ), x.is_st r) :
x.is_st x.st
theorem hyperreal.is_st_st {x : ℝ*} (hx : x.st 0) :
x.is_st x.st
theorem hyperreal.is_st_st' {x : ℝ*} (hx : ¬x.infinite) :
x.is_st x.st
theorem hyperreal.st_id_real (r : ) :
r.st = r
theorem hyperreal.eq_of_is_st_real {r s : } :
r.is_st sr = s
theorem hyperreal.is_st_real_iff_eq {r s : } :
r.is_st s r = s
theorem hyperreal.is_st_trans_real {r s t : } :
r.is_st ss.is_st tr.is_st t
theorem hyperreal.is_st_inj_real {r₁ r₂ s : } (h1 : r₁.is_st s) (h2 : r₂.is_st s) :
r₁ = r₂
theorem hyperreal.is_st_iff_abs_sub_lt_delta {x : ℝ*} {r : } :
x.is_st r ∀ (δ : ), 0 < δabs (x - r) < δ
theorem hyperreal.is_st_add {x y : ℝ*} {r s : } :
x.is_st ry.is_st s(x + y).is_st (r + s)
theorem hyperreal.is_st_neg {x : ℝ*} {r : } (hxr : x.is_st r) :
(-x).is_st (-r)
theorem hyperreal.is_st_sub {x y : ℝ*} {r s : } :
x.is_st ry.is_st s(x - y).is_st (r - s)
theorem hyperreal.lt_of_is_st_lt {x y : ℝ*} {r s : } (hxr : x.is_st r) (hys : y.is_st s) :
r < sx < y
theorem hyperreal.is_st_le_of_le {x y : ℝ*} {r s : } (hrx : x.is_st r) (hsy : y.is_st s) :
x yr s
theorem hyperreal.st_le_of_le {x y : ℝ*} (hix : ¬x.infinite) (hiy : ¬y.infinite) :
x yx.st y.st
theorem hyperreal.lt_of_st_lt {x y : ℝ*} (hix : ¬x.infinite) (hiy : ¬y.infinite) :
x.st < y.stx < y

Basic lemmas about infinite #

theorem hyperreal.infinite_pos_def {x : ℝ*} :
x.infinite_pos ∀ (r : ), r < x
theorem hyperreal.infinite_neg_def {x : ℝ*} :
x.infinite_neg ∀ (r : ), x < r
theorem hyperreal.not_infinite_add {x y : ℝ*} (hx : ¬x.infinite) (hy : ¬y.infinite) :
theorem hyperreal.not_infinite_iff_exist_lt_gt {x : ℝ*} :
¬x.infinite ∃ (r s : ), r < x x < s
theorem hyperreal.not_real_of_infinite {x : ℝ*} :
x.infinite∀ (r : ), x r

Facts about st that require some infinite machinery #

theorem hyperreal.is_st_mul {x y : ℝ*} {r s : } (hxr : x.is_st r) (hys : y.is_st s) :
(x * y).is_st (r * s)
theorem hyperreal.not_infinite_mul {x y : ℝ*} (hx : ¬x.infinite) (hy : ¬y.infinite) :
theorem hyperreal.st_add {x y : ℝ*} (hx : ¬x.infinite) (hy : ¬y.infinite) :
(x + y).st = x.st + y.st
theorem hyperreal.st_neg (x : ℝ*) :
(-x).st = -x.st
theorem hyperreal.st_mul {x y : ℝ*} (hx : ¬x.infinite) (hy : ¬y.infinite) :
(x * y).st = (x.st) * y.st

Basic lemmas about infinitesimal #

theorem hyperreal.infinitesimal_def {x : ℝ*} :
x.infinitesimal ∀ (r : ), 0 < r-r < x x < r
theorem hyperreal.lt_of_pos_of_infinitesimal {x : ℝ*} :
x.infinitesimal∀ (r : ), 0 < rx < r
theorem hyperreal.lt_neg_of_pos_of_infinitesimal {x : ℝ*} :
x.infinitesimal∀ (r : ), 0 < r-r < x
theorem hyperreal.gt_of_neg_of_infinitesimal {x : ℝ*} :
x.infinitesimal∀ (r : ), r < 0r < x
theorem hyperreal.not_real_of_infinitesimal_ne_zero (x : ℝ*) :
x.infinitesimalx 0∀ (r : ), x r
theorem hyperreal.infinitesimal_sub_is_st {x : ℝ*} {r : } (hxr : x.is_st r) :

st stuff that requires infinitesimal machinery #

theorem hyperreal.is_st_inv {x : ℝ*} {r : } (hi : ¬x.infinitesimal) :
theorem hyperreal.st_inv (x : ℝ*) :

Infinite stuff that requires infinitesimal machinery #

theorem hyperreal.infinite_mul_infinite {x y : ℝ*} :
x.infinitey.infinite(x * y).infinite