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

def Hyperreal : Type

Hyperreal numbers on the ultrafilter extending the cofinite filter

Equations

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

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 "ℝ*")

noncomputable instance Hyperreal.instLinearOrderedFieldHyperreal : LinearOrderedField ℝ*

Equations

• Hyperreal.instLinearOrderedFieldHyperreal = inferInstanceAs (LinearOrderedField (Filter.Germ ↑(Filter.hyperfilter ℕ) ℝ))

def Hyperreal.ofReal : ℝ → ℝ*

Natural embedding ℝ → ℝ*.

Equations

• Hyperreal.ofReal = Filter.Germ.const

noncomputable instance Hyperreal.instCoeTCRealHyperreal : CoeTC ℝ ℝ*

Equations

• Hyperreal.instCoeTCRealHyperreal = { 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 : ℕ) [Nat.AtLeastTwo n] : ↑(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

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 Hyperreal.ofSeq

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

noncomputable def Hyperreal.epsilon : ℝ*

A sample infinitesimal hyperreal

Equations

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

noncomputable def Hyperreal.omega : ℝ*

A sample infinite hyperreal

Equations

• Hyperreal.omega = Hyperreal.ofSeq Nat.cast

def Hyperreal.termε : Lean.ParserDescr

A sample infinitesimal hyperreal

Equations

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

def Hyperreal.termω : Lean.ParserDescr

A sample infinite hyperreal

Equations

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

@[simp]

theorem Hyperreal.inv_omega : Hyperreal.omega⁻¹ = Hyperreal.epsilon

@[simp]

theorem Hyperreal.inv_epsilon : Hyperreal.epsilon⁻¹ = Hyperreal.omega

theorem Hyperreal.omega_pos : 0 < Hyperreal.omega

theorem Hyperreal.epsilon_pos : 0 < Hyperreal.epsilon

theorem Hyperreal.epsilon_ne_zero : Hyperreal.epsilon ≠ 0

theorem Hyperreal.omega_ne_zero : Hyperreal.omega ≠ 0

theorem Hyperreal.epsilon_mul_omega : Hyperreal.epsilon * Hyperreal.omega = 1

theorem Hyperreal.lt_of_tendsto_zero_of_pos {f : ℕ → ℝ} (hf : Filter.Tendsto f Filter.atTop (nhds 0)) {r : ℝ} : 0 < r → Hyperreal.ofSeq f < ↑r

theorem Hyperreal.neg_lt_of_tendsto_zero_of_pos {f : ℕ → ℝ} (hf : Filter.Tendsto f Filter.atTop (nhds 0)) {r : ℝ} : 0 < r → -↑r < Hyperreal.ofSeq f

theorem Hyperreal.gt_of_tendsto_zero_of_neg {f : ℕ → ℝ} (hf : Filter.Tendsto f Filter.atTop (nhds 0)) {r : ℝ} : r < 0 → ↑r < Hyperreal.ofSeq f

theorem Hyperreal.epsilon_lt_pos (x : ℝ) : 0 < x → Hyperreal.epsilon < ↑x

def Hyperreal.IsSt (x : ℝ*) (r : ℝ) : Prop

Standard part predicate

Equations

• Hyperreal.IsSt x r = ∀ (δ : ℝ), 0 < δ → ↑r - ↑δ < x ∧ x < ↑r + ↑δ

noncomputable def Hyperreal.st : ℝ* → ℝ

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

Equations

• Hyperreal.st x = if h : ∃ (r : ℝ), Hyperreal.IsSt x r then Classical.choose h else 0

def Hyperreal.Infinitesimal (x : ℝ*) : Prop

A hyperreal number is infinitesimal if its standard part is 0

Equations

• Hyperreal.Infinitesimal x = Hyperreal.IsSt x 0

def Hyperreal.InfinitePos (x : ℝ*) : Prop

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

Equations

• Hyperreal.InfinitePos x = ∀ (r : ℝ), ↑r < x

def Hyperreal.InfiniteNeg (x : ℝ*) : Prop

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

Equations

• Hyperreal.InfiniteNeg x = ∀ (r : ℝ), x < ↑r

def Hyperreal.Infinite (x : ℝ*) : Prop

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

Equations

• Hyperreal.Infinite x = (Hyperreal.InfinitePos x ∨ Hyperreal.InfiniteNeg x)

Some facts about st

theorem Hyperreal.isSt_ofSeq_iff_tendsto {f : ℕ → ℝ} {r : ℝ} : Hyperreal.IsSt (Hyperreal.ofSeq f) r ↔ Filter.Tendsto f (↑(Filter.hyperfilter ℕ)) (nhds r)

theorem Hyperreal.isSt_iff_tendsto {x : ℝ*} {r : ℝ} : Hyperreal.IsSt x r ↔ Filter.Germ.Tendsto x (nhds r)

theorem Hyperreal.isSt_of_tendsto {f : ℕ → ℝ} {r : ℝ} (hf : Filter.Tendsto f Filter.atTop (nhds r)) : Hyperreal.IsSt (Hyperreal.ofSeq f) r

theorem Hyperreal.IsSt.lt {x : ℝ*} {y : ℝ*} {r : ℝ} {s : ℝ} (hxr : Hyperreal.IsSt x r) (hys : Hyperreal.IsSt y s) (hrs : r < s) : x < y

theorem Hyperreal.IsSt.unique {x : ℝ*} {r : ℝ} {s : ℝ} (hr : Hyperreal.IsSt x r) (hs : Hyperreal.IsSt x s) : r = s

theorem Hyperreal.IsSt.st_eq {x : ℝ*} {r : ℝ} (hxr : Hyperreal.IsSt x r) : Hyperreal.st x = r

theorem Hyperreal.IsSt.not_infinite {x : ℝ*} {r : ℝ} (h : Hyperreal.IsSt x r) : ¬Hyperreal.Infinite x

theorem Hyperreal.not_infinite_of_exists_st {x : ℝ*} : (∃ (r : ℝ), Hyperreal.IsSt x r) → ¬Hyperreal.Infinite x

theorem Hyperreal.Infinite.st_eq {x : ℝ*} (hi : Hyperreal.Infinite x) : Hyperreal.st x = 0

theorem Hyperreal.isSt_sSup {x : ℝ*} (hni : ¬Hyperreal.Infinite x) : Hyperreal.IsSt x (sSup {y : ℝ | ↑y < x})

theorem Hyperreal.exists_st_of_not_infinite {x : ℝ*} (hni : ¬Hyperreal.Infinite x) : ∃ (r : ℝ), Hyperreal.IsSt x r

theorem Hyperreal.st_eq_sSup {x : ℝ*} : Hyperreal.st x = sSup {y : ℝ | ↑y < x}

theorem Hyperreal.exists_st_iff_not_infinite {x : ℝ*} : (∃ (r : ℝ), Hyperreal.IsSt x r) ↔ ¬Hyperreal.Infinite x

theorem Hyperreal.infinite_iff_not_exists_st {x : ℝ*} : Hyperreal.Infinite x ↔ ¬∃ (r : ℝ), Hyperreal.IsSt x r

theorem Hyperreal.IsSt.isSt_st {x : ℝ*} {r : ℝ} (hxr : Hyperreal.IsSt x r) : Hyperreal.IsSt x (Hyperreal.st x)

theorem Hyperreal.isSt_st_of_exists_st {x : ℝ*} (hx : ∃ (r : ℝ), Hyperreal.IsSt x r) : Hyperreal.IsSt x (Hyperreal.st x)

theorem Hyperreal.isSt_st' {x : ℝ*} (hx : ¬Hyperreal.Infinite x) : Hyperreal.IsSt x (Hyperreal.st x)

theorem Hyperreal.isSt_st {x : ℝ*} (hx : Hyperreal.st x ≠ 0) : Hyperreal.IsSt x (Hyperreal.st x)

theorem Hyperreal.isSt_refl_real (r : ℝ) : Hyperreal.IsSt (↑r) r

theorem Hyperreal.st_id_real (r : ℝ) : Hyperreal.st ↑r = r

theorem Hyperreal.eq_of_isSt_real {r : ℝ} {s : ℝ} : Hyperreal.IsSt (↑r) s → r = s

theorem Hyperreal.isSt_real_iff_eq {r : ℝ} {s : ℝ} : Hyperreal.IsSt (↑r) s ↔ r = s

theorem Hyperreal.isSt_symm_real {r : ℝ} {s : ℝ} : Hyperreal.IsSt (↑r) s ↔ Hyperreal.IsSt (↑s) r

theorem Hyperreal.isSt_trans_real {r : ℝ} {s : ℝ} {t : ℝ} : Hyperreal.IsSt (↑r) s → Hyperreal.IsSt (↑s) t → Hyperreal.IsSt (↑r) t

theorem Hyperreal.isSt_inj_real {r₁ : ℝ} {r₂ : ℝ} {s : ℝ} (h1 : Hyperreal.IsSt (↑r₁) s) (h2 : Hyperreal.IsSt (↑r₂) s) : r₁ = r₂

theorem Hyperreal.isSt_iff_abs_sub_lt_delta {x : ℝ*} {r : ℝ} : Hyperreal.IsSt x r ↔ ∀ (δ : ℝ), 0 < δ → |x - ↑r| < ↑δ

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

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

theorem Hyperreal.IsSt.add {x : ℝ*} {y : ℝ*} {r : ℝ} {s : ℝ} (hxr : Hyperreal.IsSt x r) (hys : Hyperreal.IsSt y s) : Hyperreal.IsSt (x + y) (r + s)

theorem Hyperreal.IsSt.neg {x : ℝ*} {r : ℝ} (hxr : Hyperreal.IsSt x r) : Hyperreal.IsSt (-x) (-r)

theorem Hyperreal.IsSt.sub {x : ℝ*} {y : ℝ*} {r : ℝ} {s : ℝ} (hxr : Hyperreal.IsSt x r) (hys : Hyperreal.IsSt y s) : Hyperreal.IsSt (x - y) (r - s)

theorem Hyperreal.IsSt.le {x : ℝ*} {y : ℝ*} {r : ℝ} {s : ℝ} (hrx : Hyperreal.IsSt x r) (hsy : Hyperreal.IsSt y s) (hxy : x ≤ y) : r ≤ s

theorem Hyperreal.st_le_of_le {x : ℝ*} {y : ℝ*} (hix : ¬Hyperreal.Infinite x) (hiy : ¬Hyperreal.Infinite y) : x ≤ y → Hyperreal.st x ≤ Hyperreal.st y

theorem Hyperreal.lt_of_st_lt {x : ℝ*} {y : ℝ*} (hix : ¬Hyperreal.Infinite x) (hiy : ¬Hyperreal.Infinite y) : Hyperreal.st x < Hyperreal.st y → x < y

Basic lemmas about infinite

theorem Hyperreal.infinitePos_def {x : ℝ*} : Hyperreal.InfinitePos x ↔ ∀ (r : ℝ), ↑r < x

theorem Hyperreal.infiniteNeg_def {x : ℝ*} : Hyperreal.InfiniteNeg x ↔ ∀ (r : ℝ), x < ↑r

theorem Hyperreal.InfinitePos.pos {x : ℝ*} (hip : Hyperreal.InfinitePos x) : 0 < x

theorem Hyperreal.InfiniteNeg.lt_zero {x : ℝ*} : Hyperreal.InfiniteNeg x → x < 0

theorem Hyperreal.Infinite.ne_zero {x : ℝ*} (hI : Hyperreal.Infinite x) : x ≠ 0

theorem Hyperreal.not_infinite_zero : ¬Hyperreal.Infinite 0

theorem Hyperreal.InfiniteNeg.not_infinitePos {x : ℝ*} : Hyperreal.InfiniteNeg x → ¬Hyperreal.InfinitePos x

theorem Hyperreal.InfinitePos.not_infiniteNeg {x : ℝ*} (hp : Hyperreal.InfinitePos x) : ¬Hyperreal.InfiniteNeg x

theorem Hyperreal.InfinitePos.neg {x : ℝ*} : Hyperreal.InfinitePos x → Hyperreal.InfiniteNeg (-x)

theorem Hyperreal.InfiniteNeg.neg {x : ℝ*} : Hyperreal.InfiniteNeg x → Hyperreal.InfinitePos (-x)

@[simp]

theorem Hyperreal.infiniteNeg_neg {x : ℝ*} : Hyperreal.InfiniteNeg (-x) ↔ Hyperreal.InfinitePos x

@[simp]

theorem Hyperreal.infinitePos_neg {x : ℝ*} : Hyperreal.InfinitePos (-x) ↔ Hyperreal.InfiniteNeg x

@[simp]

theorem Hyperreal.infinite_neg {x : ℝ*} : Hyperreal.Infinite (-x) ↔ Hyperreal.Infinite x

theorem Hyperreal.Infinitesimal.not_infinite {x : ℝ*} (h : Hyperreal.Infinitesimal x) : ¬Hyperreal.Infinite x

theorem Hyperreal.Infinite.not_infinitesimal {x : ℝ*} (h : Hyperreal.Infinite x) : ¬Hyperreal.Infinitesimal x

theorem Hyperreal.InfinitePos.not_infinitesimal {x : ℝ*} (h : Hyperreal.InfinitePos x) : ¬Hyperreal.Infinitesimal x

theorem Hyperreal.InfiniteNeg.not_infinitesimal {x : ℝ*} (h : Hyperreal.InfiniteNeg x) : ¬Hyperreal.Infinitesimal x

theorem Hyperreal.infinitePos_iff_infinite_and_pos {x : ℝ*} : Hyperreal.InfinitePos x ↔ Hyperreal.Infinite x ∧ 0 < x

theorem Hyperreal.infiniteNeg_iff_infinite_and_neg {x : ℝ*} : Hyperreal.InfiniteNeg x ↔ Hyperreal.Infinite x ∧ x < 0

theorem Hyperreal.infinitePos_iff_infinite_of_nonneg {x : ℝ*} (hp : 0 ≤ x) : Hyperreal.InfinitePos x ↔ Hyperreal.Infinite x

theorem Hyperreal.infinitePos_iff_infinite_of_pos {x : ℝ*} (hp : 0 < x) : Hyperreal.InfinitePos x ↔ Hyperreal.Infinite x

theorem Hyperreal.infiniteNeg_iff_infinite_of_neg {x : ℝ*} (hn : x < 0) : Hyperreal.InfiniteNeg x ↔ Hyperreal.Infinite x

theorem Hyperreal.infinitePos_abs_iff_infinite_abs {x : ℝ*} : Hyperreal.InfinitePos |x| ↔ Hyperreal.Infinite |x|

@[simp]

theorem Hyperreal.infinite_abs_iff {x : ℝ*} : Hyperreal.Infinite |x| ↔ Hyperreal.Infinite x

@[simp]

theorem Hyperreal.infinitePos_abs_iff_infinite {x : ℝ*} : Hyperreal.InfinitePos |x| ↔ Hyperreal.Infinite x

theorem Hyperreal.infinite_iff_abs_lt_abs {x : ℝ*} : Hyperreal.Infinite x ↔ ∀ (r : ℝ), |↑r| < |x|

theorem Hyperreal.infinitePos_add_not_infiniteNeg {x : ℝ*} {y : ℝ*} : Hyperreal.InfinitePos x → ¬Hyperreal.InfiniteNeg y → Hyperreal.InfinitePos (x + y)

theorem Hyperreal.not_infiniteNeg_add_infinitePos {x : ℝ*} {y : ℝ*} : ¬Hyperreal.InfiniteNeg x → Hyperreal.InfinitePos y → Hyperreal.InfinitePos (x + y)

theorem Hyperreal.infiniteNeg_add_not_infinitePos {x : ℝ*} {y : ℝ*} : Hyperreal.InfiniteNeg x → ¬Hyperreal.InfinitePos y → Hyperreal.InfiniteNeg (x + y)

theorem Hyperreal.not_infinitePos_add_infiniteNeg {x : ℝ*} {y : ℝ*} : ¬Hyperreal.InfinitePos x → Hyperreal.InfiniteNeg y → Hyperreal.InfiniteNeg (x + y)

theorem Hyperreal.infinitePos_add_infinitePos {x : ℝ*} {y : ℝ*} : Hyperreal.InfinitePos x → Hyperreal.InfinitePos y → Hyperreal.InfinitePos (x + y)

theorem Hyperreal.infiniteNeg_add_infiniteNeg {x : ℝ*} {y : ℝ*} : Hyperreal.InfiniteNeg x → Hyperreal.InfiniteNeg y → Hyperreal.InfiniteNeg (x + y)

theorem Hyperreal.infinitePos_add_not_infinite {x : ℝ*} {y : ℝ*} : Hyperreal.InfinitePos x → ¬Hyperreal.Infinite y → Hyperreal.InfinitePos (x + y)

theorem Hyperreal.infiniteNeg_add_not_infinite {x : ℝ*} {y : ℝ*} : Hyperreal.InfiniteNeg x → ¬Hyperreal.Infinite y → Hyperreal.InfiniteNeg (x + y)

theorem Hyperreal.infinitePos_of_tendsto_top {f : ℕ → ℝ} (hf : Filter.Tendsto f Filter.atTop Filter.atTop) : Hyperreal.InfinitePos (Hyperreal.ofSeq f)

theorem Hyperreal.infiniteNeg_of_tendsto_bot {f : ℕ → ℝ} (hf : Filter.Tendsto f Filter.atTop Filter.atBot) : Hyperreal.InfiniteNeg (Hyperreal.ofSeq f)

theorem Hyperreal.not_infinite_neg {x : ℝ*} : ¬Hyperreal.Infinite x → ¬Hyperreal.Infinite (-x)

theorem Hyperreal.not_infinite_add {x : ℝ*} {y : ℝ*} (hx : ¬Hyperreal.Infinite x) (hy : ¬Hyperreal.Infinite y) : ¬Hyperreal.Infinite (x + y)

theorem Hyperreal.not_infinite_iff_exist_lt_gt {x : ℝ*} : ¬Hyperreal.Infinite x ↔ ∃ (r : ℝ) (s : ℝ), ↑r < x ∧ x < ↑s

theorem Hyperreal.not_infinite_real (r : ℝ) : ¬Hyperreal.Infinite ↑r

theorem Hyperreal.Infinite.ne_real {x : ℝ*} : Hyperreal.Infinite x → ∀ (r : ℝ), x ≠ ↑r

Facts about st that require some infinite machinery

theorem Hyperreal.IsSt.mul {x : ℝ*} {y : ℝ*} {r : ℝ} {s : ℝ} (hxr : Hyperreal.IsSt x r) (hys : Hyperreal.IsSt y s) : Hyperreal.IsSt (x * y) (r * s)

theorem Hyperreal.not_infinite_mul {x : ℝ*} {y : ℝ*} (hx : ¬Hyperreal.Infinite x) (hy : ¬Hyperreal.Infinite y) : ¬Hyperreal.Infinite (x * y)

theorem Hyperreal.st_add {x : ℝ*} {y : ℝ*} (hx : ¬Hyperreal.Infinite x) (hy : ¬Hyperreal.Infinite y) : Hyperreal.st (x + y) = Hyperreal.st x + Hyperreal.st y

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

theorem Hyperreal.st_mul {x : ℝ*} {y : ℝ*} (hx : ¬Hyperreal.Infinite x) (hy : ¬Hyperreal.Infinite y) : Hyperreal.st (x * y) = Hyperreal.st x * Hyperreal.st y

Basic lemmas about infinitesimal

theorem Hyperreal.infinitesimal_def {x : ℝ*} : Hyperreal.Infinitesimal x ↔ ∀ (r : ℝ), 0 < r → -↑r < x ∧ x < ↑r

theorem Hyperreal.lt_of_pos_of_infinitesimal {x : ℝ*} : Hyperreal.Infinitesimal x → ∀ (r : ℝ), 0 < r → x < ↑r

theorem Hyperreal.lt_neg_of_pos_of_infinitesimal {x : ℝ*} : Hyperreal.Infinitesimal x → ∀ (r : ℝ), 0 < r → -↑r < x

theorem Hyperreal.gt_of_neg_of_infinitesimal {x : ℝ*} (hi : Hyperreal.Infinitesimal x) (r : ℝ) (hr : r < 0) : ↑r < x

theorem Hyperreal.abs_lt_real_iff_infinitesimal {x : ℝ*} : Hyperreal.Infinitesimal x ↔ ∀ (r : ℝ), r ≠ 0 → |x| < |↑r|

theorem Hyperreal.infinitesimal_zero : Hyperreal.Infinitesimal 0

theorem Hyperreal.Infinitesimal.eq_zero {r : ℝ} : Hyperreal.Infinitesimal ↑r → r = 0

@[simp]

theorem Hyperreal.infinitesimal_real_iff {r : ℝ} : Hyperreal.Infinitesimal ↑r ↔ r = 0

theorem Hyperreal.Infinitesimal.add {x : ℝ*} {y : ℝ*} (hx : Hyperreal.Infinitesimal x) (hy : Hyperreal.Infinitesimal y) : Hyperreal.Infinitesimal (x + y)

theorem Hyperreal.Infinitesimal.neg {x : ℝ*} (hx : Hyperreal.Infinitesimal x) : Hyperreal.Infinitesimal (-x)

@[simp]

theorem Hyperreal.infinitesimal_neg {x : ℝ*} : Hyperreal.Infinitesimal (-x) ↔ Hyperreal.Infinitesimal x

theorem Hyperreal.Infinitesimal.mul {x : ℝ*} {y : ℝ*} (hx : Hyperreal.Infinitesimal x) (hy : Hyperreal.Infinitesimal y) : Hyperreal.Infinitesimal (x * y)

theorem Hyperreal.infinitesimal_of_tendsto_zero {f : ℕ → ℝ} (h : Filter.Tendsto f Filter.atTop (nhds 0)) : Hyperreal.Infinitesimal (Hyperreal.ofSeq f)

theorem Hyperreal.infinitesimal_epsilon : Hyperreal.Infinitesimal Hyperreal.epsilon

theorem Hyperreal.not_real_of_infinitesimal_ne_zero (x : ℝ*) : Hyperreal.Infinitesimal x → x ≠ 0 → ∀ (r : ℝ), x ≠ ↑r

theorem Hyperreal.IsSt.infinitesimal_sub {x : ℝ*} {r : ℝ} (hxr : Hyperreal.IsSt x r) : Hyperreal.Infinitesimal (x - ↑r)

theorem Hyperreal.infinitesimal_sub_st {x : ℝ*} (hx : ¬Hyperreal.Infinite x) : Hyperreal.Infinitesimal (x - ↑(Hyperreal.st x))

theorem Hyperreal.infinitePos_iff_infinitesimal_inv_pos {x : ℝ*} : Hyperreal.InfinitePos x ↔ Hyperreal.Infinitesimal x⁻¹ ∧ 0 < x⁻¹

theorem Hyperreal.infiniteNeg_iff_infinitesimal_inv_neg {x : ℝ*} : Hyperreal.InfiniteNeg x ↔ Hyperreal.Infinitesimal x⁻¹ ∧ x⁻¹ < 0

theorem Hyperreal.infinitesimal_inv_of_infinite {x : ℝ*} : Hyperreal.Infinite x → Hyperreal.Infinitesimal x⁻¹

theorem Hyperreal.infinite_of_infinitesimal_inv {x : ℝ*} (h0 : x ≠ 0) (hi : Hyperreal.Infinitesimal x⁻¹) : Hyperreal.Infinite x

theorem Hyperreal.infinite_iff_infinitesimal_inv {x : ℝ*} (h0 : x ≠ 0) : Hyperreal.Infinite x ↔ Hyperreal.Infinitesimal x⁻¹

theorem Hyperreal.infinitesimal_pos_iff_infinitePos_inv {x : ℝ*} : Hyperreal.InfinitePos x⁻¹ ↔ Hyperreal.Infinitesimal x ∧ 0 < x

theorem Hyperreal.infinitesimal_neg_iff_infiniteNeg_inv {x : ℝ*} : Hyperreal.InfiniteNeg x⁻¹ ↔ Hyperreal.Infinitesimal x ∧ x < 0

theorem Hyperreal.infinitesimal_iff_infinite_inv {x : ℝ*} (h : x ≠ 0) : Hyperreal.Infinitesimal x ↔ Hyperreal.Infinite x⁻¹

Hyperreal.st stuff that requires infinitesimal machinery

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

theorem Hyperreal.st_inv (x : ℝ*) : Hyperreal.st x⁻¹ = (Hyperreal.st x)⁻¹

Infinite stuff that requires infinitesimal machinery

theorem Hyperreal.infinitePos_omega : Hyperreal.InfinitePos Hyperreal.omega

theorem Hyperreal.infinite_omega : Hyperreal.Infinite Hyperreal.omega

theorem Hyperreal.infinitePos_mul_of_infinitePos_not_infinitesimal_pos {x : ℝ*} {y : ℝ*} : Hyperreal.InfinitePos x → ¬Hyperreal.Infinitesimal y → 0 < y → Hyperreal.InfinitePos (x * y)

theorem Hyperreal.infinitePos_mul_of_not_infinitesimal_pos_infinitePos {x : ℝ*} {y : ℝ*} : ¬Hyperreal.Infinitesimal x → 0 < x → Hyperreal.InfinitePos y → Hyperreal.InfinitePos (x * y)

theorem Hyperreal.infinitePos_mul_of_infiniteNeg_not_infinitesimal_neg {x : ℝ*} {y : ℝ*} : Hyperreal.InfiniteNeg x → ¬Hyperreal.Infinitesimal y → y < 0 → Hyperreal.InfinitePos (x * y)

theorem Hyperreal.infinitePos_mul_of_not_infinitesimal_neg_infiniteNeg {x : ℝ*} {y : ℝ*} : ¬Hyperreal.Infinitesimal x → x < 0 → Hyperreal.InfiniteNeg y → Hyperreal.InfinitePos (x * y)

theorem Hyperreal.infiniteNeg_mul_of_infinitePos_not_infinitesimal_neg {x : ℝ*} {y : ℝ*} : Hyperreal.InfinitePos x → ¬Hyperreal.Infinitesimal y → y < 0 → Hyperreal.InfiniteNeg (x * y)

theorem Hyperreal.infiniteNeg_mul_of_not_infinitesimal_neg_infinitePos {x : ℝ*} {y : ℝ*} : ¬Hyperreal.Infinitesimal x → x < 0 → Hyperreal.InfinitePos y → Hyperreal.InfiniteNeg (x * y)

theorem Hyperreal.infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos {x : ℝ*} {y : ℝ*} : Hyperreal.InfiniteNeg x → ¬Hyperreal.Infinitesimal y → 0 < y → Hyperreal.InfiniteNeg (x * y)

theorem Hyperreal.infiniteNeg_mul_of_not_infinitesimal_pos_infiniteNeg {x : ℝ*} {y : ℝ*} : ¬Hyperreal.Infinitesimal x → 0 < x → Hyperreal.InfiniteNeg y → Hyperreal.InfiniteNeg (x * y)

theorem Hyperreal.infinitePos_mul_infinitePos {x : ℝ*} {y : ℝ*} : Hyperreal.InfinitePos x → Hyperreal.InfinitePos y → Hyperreal.InfinitePos (x * y)

theorem Hyperreal.infiniteNeg_mul_infiniteNeg {x : ℝ*} {y : ℝ*} : Hyperreal.InfiniteNeg x → Hyperreal.InfiniteNeg y → Hyperreal.InfinitePos (x * y)

theorem Hyperreal.infinitePos_mul_infiniteNeg {x : ℝ*} {y : ℝ*} : Hyperreal.InfinitePos x → Hyperreal.InfiniteNeg y → Hyperreal.InfiniteNeg (x * y)

theorem Hyperreal.infiniteNeg_mul_infinitePos {x : ℝ*} {y : ℝ*} : Hyperreal.InfiniteNeg x → Hyperreal.InfinitePos y → Hyperreal.InfiniteNeg (x * y)

theorem Hyperreal.infinite_mul_of_infinite_not_infinitesimal {x : ℝ*} {y : ℝ*} : Hyperreal.Infinite x → ¬Hyperreal.Infinitesimal y → Hyperreal.Infinite (x * y)

theorem Hyperreal.infinite_mul_of_not_infinitesimal_infinite {x : ℝ*} {y : ℝ*} : ¬Hyperreal.Infinitesimal x → Hyperreal.Infinite y → Hyperreal.Infinite (x * y)

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