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

Hyperreal numbers on the ultrafilter extending the cofinite filter

Equations
Instances For

Hyperreal numbers on the ultrafilter extending the cofinite filter

Equations
Instances For
noncomputable instance Hyperreal.instLinearOrderedField :
Equations

Natural embedding ℝ → ℝ*.

Equations
Instances For
noncomputable instance Hyperreal.instCoeTCReal :
Equations
@[simp]
theorem Hyperreal.coe_eq_coe {x : } {y : } :
x = y x = y
theorem Hyperreal.coe_ne_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
theorem Hyperreal.coe_ne_zero {x : } :
x 0 x 0
theorem Hyperreal.coe_ne_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 : ) :
x⁻¹ = (↑x)⁻¹
@[simp]
theorem Hyperreal.coe_neg (x : ) :
(-x) = -x
@[simp]
theorem Hyperreal.coe_add (x : ) (y : ) :
(x + y) = x + y
@[simp]
theorem Hyperreal.coe_ofNat (n : ) [n.AtLeastTwo] :
(OfNat.ofNat n) =
@[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_le_coe {x : } {y : } :
x y x y
@[simp]
theorem Hyperreal.coe_lt_coe {x : } {y : } :
x < y x < y
@[simp]
theorem Hyperreal.coe_nonneg {x : } :
0 x 0 x
@[simp]
theorem Hyperreal.coe_pos {x : } :
0 < x 0 < x
@[simp]
theorem Hyperreal.coe_abs (x : ) :
|x| = |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.ofSeq (f : ) :

Construct a hyperreal number from a sequence of real numbers.

Equations
• = f
Instances For
theorem Hyperreal.ofSeq_lt_ofSeq {f : } {g : } :
∀ᶠ (n : ) in , f n < g n
noncomputable def Hyperreal.epsilon :

A sample infinitesimal hyperreal

Equations
Instances For
noncomputable def Hyperreal.omega :

A sample infinite hyperreal

Equations
Instances For

A sample infinitesimal hyperreal

Equations
Instances For

A sample infinite hyperreal

Equations
Instances For
@[simp]
@[simp]
theorem Hyperreal.lt_of_tendsto_zero_of_pos {f : } (hf : Filter.Tendsto f Filter.atTop (nhds 0)) {r : } :
0 < r < r
theorem Hyperreal.neg_lt_of_tendsto_zero_of_pos {f : } (hf : Filter.Tendsto f Filter.atTop (nhds 0)) {r : } :
0 < r
theorem Hyperreal.gt_of_tendsto_zero_of_neg {f : } (hf : Filter.Tendsto f Filter.atTop (nhds 0)) {r : } :
r < 0r <
theorem Hyperreal.epsilon_lt_pos (x : ) :
0 < x
def Hyperreal.IsSt (x : ℝ*) (r : ) :

Standard part predicate

Equations
• x.IsSt r = ∀ (δ : ), 0 < δr - δ < x x < r + δ
Instances For
noncomputable def Hyperreal.st :
ℝ*

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

Equations
• x.st = if h : ∃ (r : ), x.IsSt r then else 0
Instances For

A hyperreal number is infinitesimal if its standard part is 0

Equations
• x.Infinitesimal = x.IsSt 0
Instances For

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

Equations
• x.InfinitePos = ∀ (r : ), r < x
Instances For

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

Equations
• x.InfiniteNeg = ∀ (r : ), x < r
Instances For

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

Equations
• x.Infinite = (x.InfinitePos x.InfiniteNeg)
Instances For

### Some facts about st#

theorem Hyperreal.isSt_ofSeq_iff_tendsto {f : } {r : } :
.IsSt r Filter.Tendsto f (↑) (nhds r)
theorem Hyperreal.isSt_iff_tendsto {x : ℝ*} {r : } :
x.IsSt r
theorem Hyperreal.isSt_of_tendsto {f : } {r : } (hf : Filter.Tendsto f Filter.atTop (nhds r)) :
.IsSt r
theorem Hyperreal.IsSt.lt {x : ℝ*} {y : ℝ*} {r : } {s : } (hxr : x.IsSt r) (hys : y.IsSt s) (hrs : r < s) :
x < y
theorem Hyperreal.IsSt.unique {x : ℝ*} {r : } {s : } (hr : x.IsSt r) (hs : x.IsSt s) :
r = s
theorem Hyperreal.IsSt.st_eq {x : ℝ*} {r : } (hxr : x.IsSt r) :
x.st = r
theorem Hyperreal.IsSt.not_infinite {x : ℝ*} {r : } (h : x.IsSt r) :
¬x.Infinite
theorem Hyperreal.not_infinite_of_exists_st {x : ℝ*} :
(∃ (r : ), x.IsSt r)¬x.Infinite
theorem Hyperreal.Infinite.st_eq {x : ℝ*} (hi : x.Infinite) :
x.st = 0
theorem Hyperreal.isSt_sSup {x : ℝ*} (hni : ¬x.Infinite) :
x.IsSt (sSup {y : | y < x})
theorem Hyperreal.exists_st_of_not_infinite {x : ℝ*} (hni : ¬x.Infinite) :
∃ (r : ), x.IsSt r
theorem Hyperreal.st_eq_sSup {x : ℝ*} :
x.st = sSup {y : | y < x}
theorem Hyperreal.exists_st_iff_not_infinite {x : ℝ*} :
(∃ (r : ), x.IsSt r) ¬x.Infinite
theorem Hyperreal.infinite_iff_not_exists_st {x : ℝ*} :
x.Infinite ¬∃ (r : ), x.IsSt r
theorem Hyperreal.IsSt.isSt_st {x : ℝ*} {r : } (hxr : x.IsSt r) :
x.IsSt x.st
theorem Hyperreal.isSt_st_of_exists_st {x : ℝ*} (hx : ∃ (r : ), x.IsSt r) :
x.IsSt x.st
theorem Hyperreal.isSt_st' {x : ℝ*} (hx : ¬x.Infinite) :
x.IsSt x.st
theorem Hyperreal.isSt_st {x : ℝ*} (hx : x.st 0) :
x.IsSt x.st
theorem Hyperreal.isSt_refl_real (r : ) :
(↑r).IsSt r
theorem Hyperreal.st_id_real (r : ) :
(↑r).st = r
theorem Hyperreal.eq_of_isSt_real {r : } {s : } :
(↑r).IsSt sr = s
theorem Hyperreal.isSt_real_iff_eq {r : } {s : } :
(↑r).IsSt s r = s
theorem Hyperreal.isSt_symm_real {r : } {s : } :
(↑r).IsSt s (↑s).IsSt r
theorem Hyperreal.isSt_trans_real {r : } {s : } {t : } :
(↑r).IsSt s(↑s).IsSt t(↑r).IsSt t
theorem Hyperreal.isSt_inj_real {r₁ : } {r₂ : } {s : } (h1 : (↑r₁).IsSt s) (h2 : (↑r₂).IsSt s) :
r₁ = r₂
theorem Hyperreal.isSt_iff_abs_sub_lt_delta {x : ℝ*} {r : } :
x.IsSt r ∀ (δ : ), 0 < δ|x - r| < δ
theorem Hyperreal.IsSt.map {x : ℝ*} {r : } (hxr : x.IsSt r) {f : } (hf : ) :
theorem Hyperreal.IsSt.map₂ {x : ℝ*} {y : ℝ*} {r : } {s : } (hxr : x.IsSt r) (hys : y.IsSt s) {f : } (hf : ContinuousAt (r, s)) :
theorem Hyperreal.IsSt.add {x : ℝ*} {y : ℝ*} {r : } {s : } (hxr : x.IsSt r) (hys : y.IsSt s) :
(x + y).IsSt (r + s)
theorem Hyperreal.IsSt.neg {x : ℝ*} {r : } (hxr : x.IsSt r) :
(-x).IsSt (-r)
theorem Hyperreal.IsSt.sub {x : ℝ*} {y : ℝ*} {r : } {s : } (hxr : x.IsSt r) (hys : y.IsSt s) :
(x - y).IsSt (r - s)
theorem Hyperreal.IsSt.le {x : ℝ*} {y : ℝ*} {r : } {s : } (hrx : x.IsSt r) (hsy : y.IsSt s) (hxy : x y) :
r 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.infinitePos_def {x : ℝ*} :
x.InfinitePos ∀ (r : ), r < x
theorem Hyperreal.infiniteNeg_def {x : ℝ*} :
x.InfiniteNeg ∀ (r : ), x < r
theorem Hyperreal.InfinitePos.pos {x : ℝ*} (hip : x.InfinitePos) :
0 < x
theorem Hyperreal.InfiniteNeg.lt_zero {x : ℝ*} :
x.InfiniteNegx < 0
theorem Hyperreal.Infinite.ne_zero {x : ℝ*} (hI : x.Infinite) :
x 0
theorem Hyperreal.InfiniteNeg.not_infinitePos {x : ℝ*} :
x.InfiniteNeg¬x.InfinitePos
theorem Hyperreal.InfinitePos.not_infiniteNeg {x : ℝ*} (hp : x.InfinitePos) :
¬x.InfiniteNeg
theorem Hyperreal.InfinitePos.neg {x : ℝ*} :
x.InfinitePos(-x).InfiniteNeg
theorem Hyperreal.InfiniteNeg.neg {x : ℝ*} :
x.InfiniteNeg(-x).InfinitePos
@[simp]
theorem Hyperreal.infiniteNeg_neg {x : ℝ*} :
(-x).InfiniteNeg x.InfinitePos
@[simp]
theorem Hyperreal.infinitePos_neg {x : ℝ*} :
(-x).InfinitePos x.InfiniteNeg
@[simp]
theorem Hyperreal.infinite_neg {x : ℝ*} :
(-x).Infinite x.Infinite
theorem Hyperreal.Infinitesimal.not_infinite {x : ℝ*} (h : x.Infinitesimal) :
¬x.Infinite
theorem Hyperreal.Infinite.not_infinitesimal {x : ℝ*} (h : x.Infinite) :
¬x.Infinitesimal
theorem Hyperreal.InfinitePos.not_infinitesimal {x : ℝ*} (h : x.InfinitePos) :
¬x.Infinitesimal
theorem Hyperreal.InfiniteNeg.not_infinitesimal {x : ℝ*} (h : x.InfiniteNeg) :
¬x.Infinitesimal
theorem Hyperreal.infinitePos_iff_infinite_and_pos {x : ℝ*} :
x.InfinitePos x.Infinite 0 < x
theorem Hyperreal.infiniteNeg_iff_infinite_and_neg {x : ℝ*} :
x.InfiniteNeg x.Infinite x < 0
theorem Hyperreal.infinitePos_iff_infinite_of_nonneg {x : ℝ*} (hp : 0 x) :
x.InfinitePos x.Infinite
theorem Hyperreal.infinitePos_iff_infinite_of_pos {x : ℝ*} (hp : 0 < x) :
x.InfinitePos x.Infinite
theorem Hyperreal.infiniteNeg_iff_infinite_of_neg {x : ℝ*} (hn : x < 0) :
x.InfiniteNeg x.Infinite
theorem Hyperreal.infinitePos_abs_iff_infinite_abs {x : ℝ*} :
|x|.InfinitePos |x|.Infinite
@[simp]
theorem Hyperreal.infinite_abs_iff {x : ℝ*} :
|x|.Infinite x.Infinite
@[simp]
theorem Hyperreal.infinitePos_abs_iff_infinite {x : ℝ*} :
|x|.InfinitePos x.Infinite
theorem Hyperreal.infinite_iff_abs_lt_abs {x : ℝ*} :
x.Infinite ∀ (r : ), |r| < |x|
theorem Hyperreal.infinitePos_add_not_infiniteNeg {x : ℝ*} {y : ℝ*} :
x.InfinitePos¬y.InfiniteNeg(x + y).InfinitePos
theorem Hyperreal.not_infiniteNeg_add_infinitePos {x : ℝ*} {y : ℝ*} :
¬x.InfiniteNegy.InfinitePos(x + y).InfinitePos
theorem Hyperreal.infiniteNeg_add_not_infinitePos {x : ℝ*} {y : ℝ*} :
x.InfiniteNeg¬y.InfinitePos(x + y).InfiniteNeg
theorem Hyperreal.not_infinitePos_add_infiniteNeg {x : ℝ*} {y : ℝ*} :
¬x.InfinitePosy.InfiniteNeg(x + y).InfiniteNeg
theorem Hyperreal.infinitePos_add_infinitePos {x : ℝ*} {y : ℝ*} :
x.InfinitePosy.InfinitePos(x + y).InfinitePos
theorem Hyperreal.infiniteNeg_add_infiniteNeg {x : ℝ*} {y : ℝ*} :
x.InfiniteNegy.InfiniteNeg(x + y).InfiniteNeg
theorem Hyperreal.infinitePos_add_not_infinite {x : ℝ*} {y : ℝ*} :
x.InfinitePos¬y.Infinite(x + y).InfinitePos
theorem Hyperreal.infiniteNeg_add_not_infinite {x : ℝ*} {y : ℝ*} :
x.InfiniteNeg¬y.Infinite(x + y).InfiniteNeg
theorem Hyperreal.infinitePos_of_tendsto_top {f : } (hf : Filter.Tendsto f Filter.atTop Filter.atTop) :
.InfinitePos
theorem Hyperreal.infiniteNeg_of_tendsto_bot {f : } (hf : Filter.Tendsto f Filter.atTop Filter.atBot) :
.InfiniteNeg
theorem Hyperreal.not_infinite_neg {x : ℝ*} :
¬x.Infinite¬(-x).Infinite
theorem Hyperreal.not_infinite_add {x : ℝ*} {y : ℝ*} (hx : ¬x.Infinite) (hy : ¬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_infinite_real (r : ) :
¬(↑r).Infinite
theorem Hyperreal.Infinite.ne_real {x : ℝ*} :
x.Infinite∀ (r : ), x r

### Facts about st that require some infinite machinery #

theorem Hyperreal.IsSt.mul {x : ℝ*} {y : ℝ*} {r : } {s : } (hxr : x.IsSt r) (hys : y.IsSt s) :
(x * y).IsSt (r * s)
theorem Hyperreal.not_infinite_mul {x : ℝ*} {y : ℝ*} (hx : ¬x.Infinite) (hy : ¬y.Infinite) :
¬(x * 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 : ℝ*} (hi : x.Infinitesimal) (r : ) (hr : r < 0) :
r < x
theorem Hyperreal.abs_lt_real_iff_infinitesimal {x : ℝ*} :
x.Infinitesimal ∀ (r : ), r 0|x| < |r|
theorem Hyperreal.Infinitesimal.eq_zero {r : } :
(↑r).Infinitesimalr = 0
@[simp]
theorem Hyperreal.infinitesimal_real_iff {r : } :
(↑r).Infinitesimal r = 0
theorem Hyperreal.Infinitesimal.add {x : ℝ*} {y : ℝ*} (hx : x.Infinitesimal) (hy : y.Infinitesimal) :
(x + y).Infinitesimal
theorem Hyperreal.Infinitesimal.neg {x : ℝ*} (hx : x.Infinitesimal) :
(-x).Infinitesimal
@[simp]
theorem Hyperreal.infinitesimal_neg {x : ℝ*} :
(-x).Infinitesimal x.Infinitesimal
theorem Hyperreal.Infinitesimal.mul {x : ℝ*} {y : ℝ*} (hx : x.Infinitesimal) (hy : y.Infinitesimal) :
(x * y).Infinitesimal
theorem Hyperreal.infinitesimal_of_tendsto_zero {f : } (h : Filter.Tendsto f Filter.atTop (nhds 0)) :
.Infinitesimal
theorem Hyperreal.not_real_of_infinitesimal_ne_zero (x : ℝ*) :
x.Infinitesimalx 0∀ (r : ), x r
theorem Hyperreal.IsSt.infinitesimal_sub {x : ℝ*} {r : } (hxr : x.IsSt r) :
(x - r).Infinitesimal
theorem Hyperreal.infinitesimal_sub_st {x : ℝ*} (hx : ¬x.Infinite) :
(x - x.st).Infinitesimal
theorem Hyperreal.infinitePos_iff_infinitesimal_inv_pos {x : ℝ*} :
x.InfinitePos x⁻¹.Infinitesimal 0 < x⁻¹
theorem Hyperreal.infiniteNeg_iff_infinitesimal_inv_neg {x : ℝ*} :
x.InfiniteNeg x⁻¹.Infinitesimal x⁻¹ < 0
theorem Hyperreal.infinitesimal_inv_of_infinite {x : ℝ*} :
x.Infinitex⁻¹.Infinitesimal
theorem Hyperreal.infinite_of_infinitesimal_inv {x : ℝ*} (h0 : x 0) (hi : x⁻¹.Infinitesimal) :
x.Infinite
theorem Hyperreal.infinite_iff_infinitesimal_inv {x : ℝ*} (h0 : x 0) :
x.Infinite x⁻¹.Infinitesimal
theorem Hyperreal.infinitesimal_pos_iff_infinitePos_inv {x : ℝ*} :
x⁻¹.InfinitePos x.Infinitesimal 0 < x
theorem Hyperreal.infinitesimal_neg_iff_infiniteNeg_inv {x : ℝ*} :
x⁻¹.InfiniteNeg x.Infinitesimal x < 0
theorem Hyperreal.infinitesimal_iff_infinite_inv {x : ℝ*} (h : x 0) :
x.Infinitesimal x⁻¹.Infinite

### Hyperreal.st stuff that requires infinitesimal machinery #

theorem Hyperreal.IsSt.inv {x : ℝ*} {r : } (hi : ¬x.Infinitesimal) (hr : x.IsSt r) :
x⁻¹.IsSt r⁻¹
theorem Hyperreal.st_inv (x : ℝ*) :
x⁻¹.st = x.st⁻¹

### Infinite stuff that requires infinitesimal machinery #

theorem Hyperreal.infinitePos_mul_of_infinitePos_not_infinitesimal_pos {x : ℝ*} {y : ℝ*} :
x.InfinitePos¬y.Infinitesimal0 < y(x * y).InfinitePos
theorem Hyperreal.infinitePos_mul_of_not_infinitesimal_pos_infinitePos {x : ℝ*} {y : ℝ*} :
¬x.Infinitesimal0 < xy.InfinitePos(x * y).InfinitePos
theorem Hyperreal.infinitePos_mul_of_infiniteNeg_not_infinitesimal_neg {x : ℝ*} {y : ℝ*} :
x.InfiniteNeg¬y.Infinitesimaly < 0(x * y).InfinitePos
theorem Hyperreal.infinitePos_mul_of_not_infinitesimal_neg_infiniteNeg {x : ℝ*} {y : ℝ*} :
¬x.Infinitesimalx < 0y.InfiniteNeg(x * y).InfinitePos
theorem Hyperreal.infiniteNeg_mul_of_infinitePos_not_infinitesimal_neg {x : ℝ*} {y : ℝ*} :
x.InfinitePos¬y.Infinitesimaly < 0(x * y).InfiniteNeg
theorem Hyperreal.infiniteNeg_mul_of_not_infinitesimal_neg_infinitePos {x : ℝ*} {y : ℝ*} :
¬x.Infinitesimalx < 0y.InfinitePos(x * y).InfiniteNeg
theorem Hyperreal.infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos {x : ℝ*} {y : ℝ*} :
x.InfiniteNeg¬y.Infinitesimal0 < y(x * y).InfiniteNeg
theorem Hyperreal.infiniteNeg_mul_of_not_infinitesimal_pos_infiniteNeg {x : ℝ*} {y : ℝ*} :
¬x.Infinitesimal0 < xy.InfiniteNeg(x * y).InfiniteNeg
theorem Hyperreal.infinitePos_mul_infinitePos {x : ℝ*} {y : ℝ*} :
x.InfinitePosy.InfinitePos(x * y).InfinitePos
theorem Hyperreal.infiniteNeg_mul_infiniteNeg {x : ℝ*} {y : ℝ*} :
x.InfiniteNegy.InfiniteNeg(x * y).InfinitePos
theorem Hyperreal.infinitePos_mul_infiniteNeg {x : ℝ*} {y : ℝ*} :
x.InfinitePosy.InfiniteNeg(x * y).InfiniteNeg
theorem Hyperreal.infiniteNeg_mul_infinitePos {x : ℝ*} {y : ℝ*} :
x.InfiniteNegy.InfinitePos(x * y).InfiniteNeg
theorem Hyperreal.infinite_mul_of_infinite_not_infinitesimal {x : ℝ*} {y : ℝ*} :
x.Infinite¬y.Infinitesimal(x * y).Infinite
theorem Hyperreal.infinite_mul_of_not_infinitesimal_infinite {x : ℝ*} {y : ℝ*} :
¬x.Infinitesimaly.Infinite(x * y).Infinite
theorem Hyperreal.Infinite.mul {x : ℝ*} {y : ℝ*} :
x.Infinitey.Infinite(x * y).Infinite