mathlib3 documentation

data.real.hyperreal

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

def hyperreal  :

Hyperreal numbers on the ultrafilter extending the cofinite filter

Equations
Instances for hyperreal
@[protected, instance]
noncomputable def hyperreal.inhabited  :
@[protected, instance]
@[protected, instance]
noncomputable def hyperreal.has_coe_t  :
Equations
@[simp, norm_cast]
theorem hyperreal.coe_eq_coe {x y : } :
x = y x = y
theorem hyperreal.coe_ne_coe {x y : } :
x y x y
@[simp, norm_cast]
theorem hyperreal.coe_eq_zero {x : } :
x = 0 x = 0
@[simp, norm_cast]
theorem hyperreal.coe_eq_one {x : } :
x = 1 x = 1
@[norm_cast]
theorem hyperreal.coe_ne_zero {x : } :
x 0 x 0
@[norm_cast]
theorem hyperreal.coe_ne_one {x : } :
x 1 x 1
@[simp, norm_cast]
theorem hyperreal.coe_one  :
1 = 1
@[simp, norm_cast]
theorem hyperreal.coe_zero  :
0 = 0
@[simp, norm_cast]
theorem hyperreal.coe_inv (x : ) :
@[simp, norm_cast]
theorem hyperreal.coe_neg (x : ) :
@[simp, norm_cast]
theorem hyperreal.coe_add (x y : ) :
(x + y) = x + y
@[simp, norm_cast]
theorem hyperreal.coe_bit0 (x : ) :
@[simp, norm_cast]
theorem hyperreal.coe_bit1 (x : ) :
@[simp, norm_cast]
theorem hyperreal.coe_mul (x y : ) :
(x * y) = x * y
@[simp, norm_cast]
theorem hyperreal.coe_div (x y : ) :
(x / y) = x / y
@[simp, norm_cast]
theorem hyperreal.coe_sub (x y : ) :
(x - y) = x - y
@[simp, norm_cast]
theorem hyperreal.coe_le_coe {x y : } :
x y x y
@[simp, norm_cast]
theorem hyperreal.coe_lt_coe {x y : } :
x < y x < y
@[simp, norm_cast]
theorem hyperreal.coe_nonneg {x : } :
0 x 0 x
@[simp, norm_cast]
theorem hyperreal.coe_pos {x : } :
0 < x 0 < x
@[simp, norm_cast]
theorem hyperreal.coe_abs (x : ) :
@[simp, norm_cast]
@[simp, norm_cast]
noncomputable def hyperreal.of_seq (f : ) :

Construct a hyperreal number from a sequence of real numbers.

Equations
noncomputable def hyperreal.epsilon  :

A sample infinitesimal hyperreal

Equations
noncomputable def hyperreal.omega  :

A sample infinite hyperreal

Equations
def hyperreal.is_st (x : ℝ*) (r : ) :
Prop

Standard part predicate

Equations
noncomputable 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.is_st_Sup {x : ℝ*} (hni : ¬x.infinite) :
x.is_st (has_Sup.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 = has_Sup.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 s r = s
theorem hyperreal.is_st_real_iff_eq {r s : } :
r.is_st s r = s
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 < δ |x - r| < δ
theorem hyperreal.is_st_add {x y : ℝ*} {r s : } :
x.is_st r y.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 r y.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 < s x < y
theorem hyperreal.is_st_le_of_le {x y : ℝ*} {r s : } (hrx : x.is_st r) (hsy : y.is_st s) :
x y r s
theorem hyperreal.st_le_of_le {x y : ℝ*} (hix : ¬x.infinite) (hiy : ¬y.infinite) :
x y x.st y.st
theorem hyperreal.lt_of_st_lt {x y : ℝ*} (hix : ¬x.infinite) (hiy : ¬y.infinite) :
x.st < y.st x < y

Basic lemmas about infinite #

theorem hyperreal.not_infinite_add {x y : ℝ*} (hx : ¬x.infinite) (hy : ¬y.infinite) :

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.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 #

Extension for the positivity tactic: cast from to ℝ*.