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
@[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  :
()ℝ*

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  :
ℝ* → Prop

Standard part predicate

Equations
def hyperreal.st  :
ℝ*

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

Equations
def hyperreal.infinitesimal  :
ℝ* → Prop

A hyperreal number is infinitesimal if its standard part is 0

Equations
def hyperreal.infinite_pos  :
ℝ* → Prop

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

Equations
def hyperreal.infinite_neg  :
ℝ* → Prop

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

Equations
def hyperreal.infinite  :
ℝ* → 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 : } :
x.is_st rx.is_st sr = s

theorem hyperreal.not_infinite_of_exists_st {x : ℝ*} :
(∃ (r : ), x.is_st r)¬x.infinite

theorem hyperreal.is_st_Sup {x : ℝ*} :
¬x.infinitex.is_st (Sup {y : | y < x})

theorem hyperreal.exists_st_of_not_infinite {x : ℝ*} :
¬x.infinite(∃ (r : ), x.is_st r)

theorem hyperreal.st_eq_Sup {x : ℝ*} :
x.st = Sup {y : | y < x}

theorem hyperreal.st_infinite {x : ℝ*} :
x.infinitex.st = 0

theorem hyperreal.st_of_is_st {x : ℝ*} {r : } :
x.is_st rx.st = r

theorem hyperreal.is_st_st_of_is_st {x : ℝ*} {r : } :
x.is_st rx.is_st x.st

theorem hyperreal.is_st_st_of_exists_st {x : ℝ*} :
(∃ (r : ), x.is_st r)x.is_st x.st

theorem hyperreal.is_st_st {x : ℝ*} :
x.st 0x.is_st x.st

theorem hyperreal.is_st_st' {x : ℝ*} :
¬x.infinitex.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 : } :
r₁.is_st sr₂.is_st sr₁ = 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 : } :
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 : } :
x.is_st ry.is_st sr < sx < y

theorem hyperreal.is_st_le_of_le {x y : ℝ*} {r s : } :
x.is_st ry.is_st sx yr s

theorem hyperreal.st_le_of_le {x y : ℝ*} :
¬x.infinite¬y.infinitex yx.st y.st

theorem hyperreal.lt_of_st_lt {x y : ℝ*} :
¬x.infinite¬y.infinitex.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 : ℝ*} :
¬x.infinite¬y.infinite¬(x + 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 : ℝ*} (a : x.infinite) (r : ) :
x r

Facts about st that require some infinite machinery

theorem hyperreal.is_st_mul {x y : ℝ*} {r s : } :
x.is_st ry.is_st s(x * y).is_st (r * s)

theorem hyperreal.not_infinite_mul {x y : ℝ*} :
¬x.infinite¬y.infinite¬(x * y).infinite

theorem hyperreal.st_add {x y : ℝ*} :
¬x.infinite¬y.infinite(x + y).st = x.st + y.st

theorem hyperreal.st_neg (x : ℝ*) :
(-x).st = -x.st

theorem hyperreal.st_mul {x y : ℝ*} :
¬x.infinite¬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 : ℝ*} (a : x.infinitesimal) (r : ) :
0 < rx < r

theorem hyperreal.lt_neg_of_pos_of_infinitesimal {x : ℝ*} (a : x.infinitesimal) (r : ) :
0 < r-r < x

theorem hyperreal.gt_of_neg_of_infinitesimal {x : ℝ*} (a : x.infinitesimal) (r : ) :
r < 0r < x

theorem hyperreal.not_real_of_infinitesimal_ne_zero (x : ℝ*) (a : x.infinitesimal) (a_1 : x 0) (r : ) :
x r

st stuff that requires infinitesimal machinery

theorem hyperreal.is_st_inv {x : ℝ*} {r : } :

theorem hyperreal.st_inv (x : ℝ*) :

Infinite stuff that requires infinitesimal machinery

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