Documentation

Mathlib.Data.Real.Hyperreal

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

Hyperreal numbers on the ultrafilter extending the cofinite filter

Equations

Hyperreal numbers on the ultrafilter extending the cofinite filter

Equations
noncomputable def Hyperreal.ofReal :
ℝ*

Natural embedding ℝ → ℝ*.

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]
@[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
noncomputable def Hyperreal.ofSeq (f : ) :

Construct a hyperreal number from a sequence of real numbers.

Equations
theorem Hyperreal.ofSeq_lt_ofSeq {f g : } :
ofSeq f < ofSeq g ∀ᶠ (n : ) in (Filter.hyperfilter ), f n < g n
noncomputable def Hyperreal.epsilon :

A sample infinitesimal hyperreal

Equations
noncomputable def Hyperreal.omega :

A sample infinite hyperreal

Equations

A sample infinitesimal hyperreal

Equations

A sample infinite hyperreal

Equations
theorem Hyperreal.lt_of_tendsto_zero_of_pos {f : } (hf : Filter.Tendsto f Filter.atTop (nhds 0)) {r : } :
0 < rofSeq f < r
theorem Hyperreal.neg_lt_of_tendsto_zero_of_pos {f : } (hf : Filter.Tendsto f Filter.atTop (nhds 0)) {r : } :
0 < r-r < ofSeq f
theorem Hyperreal.gt_of_tendsto_zero_of_neg {f : } (hf : Filter.Tendsto f Filter.atTop (nhds 0)) {r : } :
r < 0r < ofSeq f
theorem Hyperreal.epsilon_lt_pos (x : ) :
0 < xepsilon < x
def Hyperreal.IsSt (x : ℝ*) (r : ) :

Standard part predicate

Equations
noncomputable def Hyperreal.st :
ℝ*

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

Equations

A hyperreal number is infinitesimal if its standard part is 0

Equations

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

Equations

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

Equations

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

Equations

Some facts about st #

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) :
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.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 : ContinuousAt f r) :
IsSt (Filter.Germ.map f x) (f r)
theorem Hyperreal.IsSt.map₂ {x y : ℝ*} {r s : } (hxr : x.IsSt r) (hys : y.IsSt s) {f : } (hf : ContinuousAt (Function.uncurry f) (r, s)) :
IsSt (Filter.Germ.map₂ f x y) (f 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.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.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) :
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.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

Hyperreal.st stuff that requires infinitesimal machinery #

theorem Hyperreal.IsSt.inv {x : ℝ*} {r : } (hi : ¬x.Infinitesimal) (hr : x.IsSt r) :

Infinite stuff that requires infinitesimal machinery #

theorem Hyperreal.Infinite.mul {x y : ℝ*} :
x.Infinitey.Infinite(x * y).Infinite