Construction of the hyperreal numbers as an ultraproduct of real sequences

We define the Hyperreal numbers as quotients of sequences ℕ → ℝ by an ultrafilter. These form a field, and we prove some of their basic properties.

Note that most of the machinery that is usually defined for the specific purpose of non-standard analysis (infinitesimal and infinite elements, standard parts) has been generalized to other non-archimedean fields. In particular:

• ArchimedeanClass can be used to measure whether an element is infinitesimal (0 < mk x) or infinite (mk x < 0).
• ArchimedeanClass.stdPart generalizes the standard part function to a general ordered field.

TODO

Use Łoś's Theorem FirstOrder.Language.Ultraproduct.sentence_realize to formalize the transfer principle on Hyperreal.

def Hyperreal : Type

Hyperreal numbers on the ultrafilter extending the cofinite filter.

Equations

• ℝ* = (↑(Filter.hyperfilter ℕ)).Germ ℝ

@[instance_reducible]

noncomputable instance instInhabitedHyperreal : Inhabited ℝ*

Equations

• instInhabitedHyperreal = { default := instInhabitedHyperreal._aux_1 }

def Hyperreal.«termℝ*» : Lean.ParserDescr

Hyperreal numbers on the ultrafilter extending the cofinite filter.

Equations

• Hyperreal.«termℝ*» = Lean.ParserDescr.node `Hyperreal.«termℝ*» 1024 (Lean.ParserDescr.symbol "ℝ*")

@[instance_reducible]

noncomputable instance Hyperreal.instField : Field ℝ*

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance Hyperreal.instLinearOrder : LinearOrder ℝ*

Equations

• One or more equations did not get rendered due to their size.

instance Hyperreal.instIsStrictOrderedRing : IsStrictOrderedRing ℝ*

noncomputable def Hyperreal.ofReal : ℝ → ℝ*

Natural embedding ℝ → ℝ*.

Equations

• Hyperreal.ofReal = Filter.Germ.const

@[instance_reducible]

noncomputable instance Hyperreal.instCoeTCReal : CoeTC ℝ ℝ*

Equations

• Hyperreal.instCoeTCReal = { coe := Hyperreal.ofReal }

@[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) = 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

noncomputable def Hyperreal.coeRingHom : ℝ →+*o ℝ*

The canonical map ℝ → ℝ* as an OrderRingHom.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Hyperreal.coeRingHom_toFun (x : ℝ) : coeRingHom x = ↑x

@[simp]

theorem Hyperreal.archimedeanClassMk_coe_nonneg (x : ℝ) : 0 ≤ ArchimedeanClass.mk ↑x

@[simp]

theorem Hyperreal.archimdeanClassMk_coe {x : ℝ} (hx : x ≠ 0) : ArchimedeanClass.mk ↑x = 0

@[simp]

theorem Hyperreal.stdPart_coe (x : ℝ) : ArchimedeanClass.stdPart ↑x = x

Basic constants

noncomputable def Hyperreal.ofSeq (f : ℕ → ℝ) : ℝ*

Construct a hyperreal number from a sequence of real numbers.

Equations

• Hyperreal.ofSeq f = ↑f

theorem Hyperreal.ofSeq_surjective : Function.Surjective ofSeq

theorem Hyperreal.ofSeq_lt_ofSeq {f g : ℕ → ℝ} : ofSeq f < ofSeq g ↔ ∀ᶠ (n : ℕ) in ↑(Filter.hyperfilter ℕ), f n < g n

theorem Hyperreal.ofSeq_le_ofSeq {f g : ℕ → ℝ} : ofSeq f ≤ ofSeq g ↔ ∀ᶠ (n : ℕ) in ↑(Filter.hyperfilter ℕ), f n ≤ g n

ω

noncomputable def Hyperreal.omega : ℝ*

A sample infinite hyperreal ω = ⟦(0, 1, 2, 3, ⋯)⟧.

Conventions for notations in identifiers:

• The recommended spelling of ω in identifiers is omega.

Equations

• Hyperreal.omega = Hyperreal.ofSeq Nat.cast

def Hyperreal.termω : Lean.ParserDescr

A sample infinite hyperreal ω = ⟦(0, 1, 2, 3, ⋯)⟧.

Conventions for notations in identifiers:

• The recommended spelling of ω in identifiers is omega.

Equations

• Hyperreal.termω = Lean.ParserDescr.node `Hyperreal.termω 1024 (Lean.ParserDescr.symbol "ω")

theorem Hyperreal.coe_lt_omega (r : ℝ) : ↑r < omega

theorem Hyperreal.omega_pos : 0 < omega

@[simp]

theorem Hyperreal.omega_ne_zero : omega ≠ 0

@[simp]

theorem Hyperreal.abs_omega : |omega| = omega

@[simp]

theorem Hyperreal.archimedeanClassMk_omega_neg : ArchimedeanClass.mk omega < 0

@[simp]

theorem Hyperreal.stdPart_omega : ArchimedeanClass.stdPart omega = 0

ε

noncomputable def Hyperreal.epsilon : ℝ*

A sample infinitesimal hyperreal ε = ⟦(0, 1, 1/2, 1/3, ⋯)⟧.

Conventions for notations in identifiers:

• The recommended spelling of ε in identifiers is epsilon.

Equations

• Hyperreal.epsilon = Hyperreal.ofSeq fun (n : ℕ) => (↑n)⁻¹

def Hyperreal.termε : Lean.ParserDescr

A sample infinitesimal hyperreal ε = ⟦(0, 1, 1/2, 1/3, ⋯)⟧.

Conventions for notations in identifiers:

• The recommended spelling of ε in identifiers is epsilon.

Equations

• Hyperreal.termε = Lean.ParserDescr.node `Hyperreal.termε 1024 (Lean.ParserDescr.symbol "ε")

@[simp]

theorem Hyperreal.inv_omega : omega⁻¹ = epsilon

@[simp]

theorem Hyperreal.inv_epsilon : epsilon⁻¹ = omega

@[simp]

theorem Hyperreal.epsilon_pos : 0 < epsilon

@[simp]

theorem Hyperreal.epsilon_ne_zero : epsilon ≠ 0

@[simp]

theorem Hyperreal.epsilon_mul_omega : epsilon * omega = 1

@[simp]

theorem Hyperreal.archimedeanClassMk_epsilon_pos : 0 < ArchimedeanClass.mk epsilon

Some facts about Tendsto

@[simp]

theorem Hyperreal.tendsto_ofSeq {f : ℕ → ℝ} {lb : Filter ℝ} : Filter.Germ.Tendsto (ofSeq f) lb ↔ Filter.Tendsto f (↑(Filter.hyperfilter ℕ)) lb

theorem Hyperreal.stdPart_map {x : ℝ*} {r : ℝ} {f : ℝ → ℝ} (hf : ContinuousAt f r) (hxr : Filter.Germ.Tendsto x (nhds r)) : (Filter.Germ.map f x).Tendsto (nhds (f r))

theorem Hyperreal.stdPart_map₂ {x y : ℝ*} {r s : ℝ} {f : ℝ → ℝ → ℝ} (hxr : Filter.Germ.Tendsto x (nhds r)) (hys : Filter.Germ.Tendsto y (nhds s)) (hf : ContinuousAt (Function.uncurry f) (r, s)) : (Filter.Germ.map₂ f x y).Tendsto (nhds (f r s))

theorem Hyperreal.tendsto_iff_forall {x : ℝ*} {r : ℝ} : Filter.Germ.Tendsto x (nhds r) ↔ (∀ s < r, ↑s ≤ x) ∧ ∀ s > r, x ≤ ↑s

theorem Hyperreal.archimedeanClassMk_nonneg_of_tendsto {x : ℝ*} {r : ℝ} (hx : Filter.Germ.Tendsto x (nhds r)) : 0 ≤ ArchimedeanClass.mk x

theorem Hyperreal.stdPart_of_tendsto {x : ℝ*} {r : ℝ} (hx : Filter.Germ.Tendsto x (nhds r)) : ArchimedeanClass.stdPart x = r

theorem Hyperreal.archimedeanClassMk_pos_of_tendsto {x : ℝ*} (hx : Filter.Germ.Tendsto x (nhds 0)) : 0 < ArchimedeanClass.mk x

@[simp]

theorem Hyperreal.stdPart_epsilon : ArchimedeanClass.stdPart epsilon = 0

theorem Hyperreal.epsilon_lt_of_pos {r : ℝ} : 0 < r → epsilon < ↑r

theorem Hyperreal.epsilon_lt_of_neg {r : ℝ} : r < 0 → ↑r < epsilon

theorem Hyperreal.lt_of_tendsto_atTop {x : ℝ*} (r : ℝ) (hx : Filter.Germ.Tendsto x Filter.atTop) : ↑r < x

theorem Hyperreal.lt_of_tendsto_atBot {x : ℝ*} (r : ℝ) (hx : Filter.Germ.Tendsto x Filter.atBot) : x < ↑r

theorem Hyperreal.archimedeanClassMk_neg_of_tendsto_atTop {x : ℝ*} (hx : Filter.Germ.Tendsto x Filter.atTop) : ArchimedeanClass.mk x < 0

theorem Hyperreal.archimedeanClassMk_neg_of_tendsto_atBot {x : ℝ*} (hx : Filter.Germ.Tendsto x Filter.atBot) : ArchimedeanClass.mk x < 0

theorem Hyperreal.tendsto_atTop_iff {x : ℝ*} : Filter.Germ.Tendsto x Filter.atTop ↔ 0 < x ∧ ArchimedeanClass.mk x < 0

theorem Hyperreal.tendsto_atBot_iff {x : ℝ*} : Filter.Germ.Tendsto x Filter.atBot ↔ x < 0 ∧ ArchimedeanClass.mk x < 0