@[reducible, inline]

abbrev PositiveHyperreal : Type

Equations

• PositiveHyperreal = { x : ℝ* // 0 < x }

noncomputable def Real.toPositiveHyperreal (x : ℝ) (hx : 0 < x) : PositiveHyperreal

Equations

• x.toPositiveHyperreal hx = ⟨↑x, ⋯⟩

@[simp]

theorem Real.toPositiveHyperreal_coe (x : ℝ) (hx : 0 < x) : ↑(x.toPositiveHyperreal hx) = ↑x

def PositiveHyperreal.asym_preorder : Preorder PositiveHyperreal

The asymptotic preorder in the positive hyperreals.

Equations

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

@[reducible, inline]

abbrev PositiveHyperreal.lesssim (X Y : PositiveHyperreal) : Prop

Equations

• X.lesssim Y = (X ≤ Y)

@[reducible, inline]

abbrev PositiveHyperreal.ll (X Y : PositiveHyperreal) : Prop

Equations

• X.ll Y = (X < Y)

@[reducible, inline]

abbrev PositiveHyperreal.gtrsim (X Y : PositiveHyperreal) : Prop

Equations

• X.gtrsim Y = (Y ≤ X)

@[reducible, inline]

abbrev PositiveHyperreal.gg (X Y : PositiveHyperreal) : Prop

Equations

• X.gg Y = (Y < X)

@[reducible, inline]

abbrev PositiveHyperreal.asymp (X Y : PositiveHyperreal) : Prop

Equations

• X.asymp Y = (X.lesssim Y ∧ Y.lesssim X)

@[reducible, inline]

abbrev OrderOfMagnitude : Type

Equations

• OrderOfMagnitude = OrderQuotient PositiveHyperreal.asym_preorder

@[reducible, inline]

abbrev PositiveHyperreal.order (X : PositiveHyperreal) : OrderOfMagnitude

Equations

• X.order = PositiveHyperreal.asym_preorder.quotient X

theorem PositiveHyperreal.order_surjective : Function.Surjective order

theorem PositiveHyperreal.order_eq_iff {X Y : PositiveHyperreal} : X.order = Y.order ↔ X.asymp Y

theorem PositiveHyperreal.order_le_iff {X Y : PositiveHyperreal} : X.order ≤ Y.order ↔ X.lesssim Y

theorem PositiveHyperreal.order_lt_iff {X Y : PositiveHyperreal} : X.order < Y.order ↔ X.ll Y

noncomputable instance OrderOfMagnitude.linearOrder : LinearOrder OrderOfMagnitude

Equations

• OrderOfMagnitude.linearOrder = PositiveHyperreal.asym_preorder.quot_linear OrderOfMagnitude.linearOrder._proof_5

noncomputable instance OrderOfMagnitude.one : One OrderOfMagnitude

Equations

• OrderOfMagnitude.one = { one := PositiveHyperreal.order 1 }

@[simp]

theorem PositiveHyperreal.order_one : order 1 = 1

@[simp]

theorem Real.order_of_pos (x : ℝ) (hx : 0 < x) : (x.toPositiveHyperreal hx).order = 1

noncomputable instance OrderOfMagnitude.add : Add OrderOfMagnitude

Equations

• OrderOfMagnitude.add = { add := Quotient.lift₂ (fun (x y : PositiveHyperreal) => (x + y).order) OrderOfMagnitude.add._proof_10 }

@[simp]

theorem PositiveHyperreal.order_add (X Y : PositiveHyperreal) : (X + Y).order = X.order + Y.order

@[simp]

theorem OrderOfMagnitude.add_eq_max (X Y : OrderOfMagnitude) : X + Y = max X Y

noncomputable instance OrderOfMagnitude.addCommSemigroup : AddCommSemigroup OrderOfMagnitude

Equations

• OrderOfMagnitude.addCommSemigroup = { toAdd := OrderOfMagnitude.add, add_assoc := OrderOfMagnitude.addCommSemigroup._proof_11, add_comm := OrderOfMagnitude.addCommSemigroup._proof_12 }

theorem OrderOfMagnitude.add_self (X : OrderOfMagnitude) : X + X = X

noncomputable instance OrderOfMagnitude.mul : Mul OrderOfMagnitude

Equations

• OrderOfMagnitude.mul = { mul := Quotient.lift₂ (fun (x y : PositiveHyperreal) => (x * y).order) OrderOfMagnitude.mul._proof_13 }

@[simp]

theorem PositiveHyperreal.order_mul (X Y : PositiveHyperreal) : (X * Y).order = X.order * Y.order

noncomputable instance Hyperreal.pow : Pow ℝ* ℝ*

Equations

• Hyperreal.pow = { pow := Filter.Germ.map₂ Real.rpow }

@[reducible, inline]

noncomputable abbrev to_hyperreal (x : ℕ → ℝ) : ℝ*

Equations

• to_hyperreal x = ↑x

theorem to_hyperreal_surjective : Function.Surjective to_hyperreal

noncomputable instance pow_fn : Pow (ℕ → ℝ) (ℕ → ℝ)

Equations

• pow_fn = { pow := fun (x y : ℕ → ℝ) (n : ℕ) => x n ^ y n }

@[simp]

theorem pow_fn_eq (x y : ℕ → ℝ) (n : ℕ) : (x ^ y) n = x n ^ y n

@[simp]

theorem pow_fn_zero (x : ℕ → ℝ) : x ^ 0 = 1

@[simp]

theorem Hyperreal.coe_pow (x y : ℕ → ℝ) : to_hyperreal x ^ to_hyperreal y = to_hyperreal (x ^ y)

theorem Hyperreal.coe_pow' (x y : ℝ) : ↑x ^ ↑y = ↑(x ^ y)

@[simp]

theorem Hyperreal.coe_mul_fn (x y : ℕ → ℝ) : to_hyperreal x * to_hyperreal y = to_hyperreal (x * y)

@[simp]

theorem Hyperreal.coe_add_fn (x y : ℕ → ℝ) : to_hyperreal x + to_hyperreal y = to_hyperreal (x + y)

@[simp]

theorem Hyperreal.coe_zero_fn : to_hyperreal 0 = 0

@[simp]

theorem Hyperreal.coe_one_fn : to_hyperreal 1 = 1

theorem Hyperreal.lt_def : (fun (x1 x2 : ℝ*) => x1 < x2) = Filter.Germ.LiftRel fun (x1 x2 : ℝ) => x1 < x2

theorem Hyperreal.le_def : (fun (x1 x2 : ℝ*) => x1 ≤ x2) = Filter.Germ.LiftRel fun (x1 x2 : ℝ) => x1 ≤ x2

theorem Hyperreal.gt_def : (fun (x1 x2 : ℝ*) => x1 > x2) = Filter.Germ.LiftRel fun (x1 x2 : ℝ) => x1 > x2

theorem Hyperreal.ge_def : (fun (x1 x2 : ℝ*) => x1 ≥ x2) = Filter.Germ.LiftRel fun (x1 x2 : ℝ) => x1 ≥ x2

theorem Hyperreal.pow_of_pos {x : ℝ*} (y : ℝ*) : x > 0 → x ^ y > 0

@[simp]

theorem Hyperreal.pow_of_one (y : ℝ*) : 1 ^ y = 1

noncomputable instance PositiveHyperreal.pow : Pow PositiveHyperreal ℝ*

Equations

• PositiveHyperreal.pow = { pow := fun (X : PositiveHyperreal) (y : ℝ*) => ⟨↑X ^ y, ⋯⟩ }

@[simp]

theorem PositiveHyperreal.pow_coe (X : PositiveHyperreal) (y : ℝ*) : ↑(X ^ y) = ↑X ^ y

theorem Hyperreal.pow_le_pow {x y z : ℝ*} (hx : x ≥ 0) (hz : z ≥ 0) (hxy : x ≤ y) : x ^ z ≤ y ^ z

theorem Hyperreal.pow_le_pow' {x y z : ℝ*} (hx : x > 0) (hz : z ≤ 0) (hxy : x ≤ y) : x ^ z ≥ y ^ z

theorem Hyperreal.mul_pow {x y : ℝ*} (hx : x ≥ 0) (hy : y ≥ 0) (z : ℝ*) : (x * y) ^ z = x ^ z * y ^ z

theorem Hyperreal.pow_add {x : ℝ*} (hx : x > 0) (y z : ℝ*) : x ^ (y + z) = x ^ y * x ^ z

theorem Hyperreal.pow_mul {x : ℝ*} (hx : x > 0) (y z : ℝ*) : x ^ (y * z) = (x ^ y) ^ z

@[simp]

theorem Hyperreal.pow_zero (x : ℝ*) : x ^ 0 = 1

@[simp]

theorem Hyperreal.pow_one (x : ℝ*) : x ^ 1 = x

noncomputable instance OrderOfMagnitude.pow : Pow OrderOfMagnitude ℝ

Equations

• OrderOfMagnitude.pow = { pow := fun (X : OrderOfMagnitude) (y : ℝ) => Quotient.lift (fun (x : PositiveHyperreal) => (x ^ ↑y).order) ⋯ X }

@[simp]

theorem PositiveHyperreal.order_pow (X : PositiveHyperreal) (y : ℝ) : (X ^ ↑y).order = X.order ^ y

@[simp]

theorem OrderOfMagnitude.pow_one (X : OrderOfMagnitude) : X ^ 1 = X

@[simp]

theorem OrderOfMagnitude.pow_zero (X : OrderOfMagnitude) : X ^ 0 = 1

noncomputable instance OrderOfMagnitude.inv : Inv OrderOfMagnitude

Equations

• OrderOfMagnitude.inv = { inv := fun (X : OrderOfMagnitude) => X ^ (-1) }

noncomputable instance OrderOfMagnitude.group : Group OrderOfMagnitude

Equations

• OrderOfMagnitude.group = Group.ofLeftAxioms OrderOfMagnitude.group._proof_20 OrderOfMagnitude.group._proof_21 OrderOfMagnitude.group._proof_22

@[simp]

theorem OrderOfMagnitude.div_eq (X Y : OrderOfMagnitude) : X / Y = X * Y ^ (-1)

noncomputable instance OrderOfMagnitude.comm_group : CommGroup OrderOfMagnitude

Equations

• OrderOfMagnitude.comm_group = { toGroup := OrderOfMagnitude.group, mul_comm := OrderOfMagnitude.comm_group._proof_23 }

instance OrderOfMagnitude.orderedMonoid : IsOrderedMonoid OrderOfMagnitude

noncomputable instance OrderOfMagnitude.distrib : Distrib OrderOfMagnitude

Equations

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

theorem power_i (X Y : OrderOfMagnitude) (α : ℝ) : (X * Y) ^ α = X ^ α * Y ^ α

theorem power_i' (X Y : OrderOfMagnitude) (α : ℝ) : (X / Y) ^ α = X ^ α / Y ^ α

theorem power_ii {β : ℝ} (X : OrderOfMagnitude) (α : ℝ) : X ^ (α * β) = (X ^ α) ^ β

@[simp]

theorem power_iv (α : ℝ) : 1 ^ α = 1

theorem power_vi {X Y : OrderOfMagnitude} {α : ℝ} (hα : α ≥ 0) (hXY : X ≤ Y) : X ^ α ≤ Y ^ α

theorem power_v (X Y : OrderOfMagnitude) {α : ℝ} (hα : α ≥ 0) : (X + Y) ^ α = X ^ α + Y ^ α

theorem power_vii (X Y : OrderOfMagnitude) {α : ℝ} (hα : α > 0) : X ≤ Y ↔ X ^ α ≤ Y ^ α

theorem power_vii' (X Y : OrderOfMagnitude) {α : ℝ} (hα : α > 0) : X < Y ↔ X ^ α < Y ^ α

theorem power_viii {X Y : OrderOfMagnitude} {α : ℝ} (hα : α ≤ 0) (hXY : X ≤ Y) : X ^ α ≥ Y ^ α

theorem power_ix (X Y : OrderOfMagnitude) {α : ℝ} (hα : α < 0) : X ≤ Y ↔ X ^ α ≥ Y ^ α

theorem power_ix' (X Y : OrderOfMagnitude) {α : ℝ} (hα : α < 0) : X < Y ↔ X ^ α > Y ^ α

theorem power_x (X : OrderOfMagnitude) (α β : ℝ) : X ^ (α + β) = X ^ α * X ^ β

@[reducible, inline]

abbrev LogOrderOfMagnitude : Type

Equations

• LogOrderOfMagnitude = Additive OrderOfMagnitude

@[reducible, inline]

abbrev OrderOfMagnitude.log : OrderOfMagnitude ≃ LogOrderOfMagnitude

Equations

• OrderOfMagnitude.log = Additive.ofMul

@[reducible, inline]

abbrev LogOrderOfMagnitude.exp : LogOrderOfMagnitude ≃ OrderOfMagnitude

Equations

• LogOrderOfMagnitude.exp = OrderOfMagnitude.log.symm

def OrderOfMagnitude.log_ordered : OrderOfMagnitude ≃o LogOrderOfMagnitude

Equations

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

def LogOrderOfMagnitude.exp_ordered : LogOrderOfMagnitude ≃o OrderOfMagnitude

Equations

• LogOrderOfMagnitude.exp_ordered = OrderOfMagnitude.log_ordered.symm

noncomputable instance LogOrderOfMagnitude.linear_order : LinearOrder LogOrderOfMagnitude

Equations

• LogOrderOfMagnitude.linear_order = Additive.linearOrder

@[simp]

theorem OrderOfMagnitude.log_mul (X Y : OrderOfMagnitude) : log (X * Y) = log X + log Y

@[simp]

theorem OrderOfMagnitude.log_add (X Y : OrderOfMagnitude) : log (X + Y) = max (log X) (log Y)

@[simp]

theorem OrderOfMagnitude.log_div (X Y : OrderOfMagnitude) : log (X / Y) = log X - log Y

@[simp]

theorem OrderOfMagnitude.log_one : log 1 = 0

theorem OrderOfMagnitude.log_const (C : ℝ) (hC : C > 0) : log (C.toPositiveHyperreal hC).order = 0

noncomputable instance LogOrderOfMagnitude.vec : Module ℝ LogOrderOfMagnitude

Equations

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

theorem LogOrderOfMagnitude.smul_def (α : ℝ) (x : LogOrderOfMagnitude) : α • x = OrderOfMagnitude.log (exp x ^ α)

instance LogOrderOfMagnitude.posSMulStrictMono : PosSMulStrictMono ℝ LogOrderOfMagnitude

@[simp]

theorem OrderOfMagnitude.log_pow (X : OrderOfMagnitude) (α : ℝ) : log (X ^ α) = α • log X

@[reducible, inline]

abbrev internal (E : ℕ → Set ℝ) : Set ℝ*

Equations

• internal E = Filter.Germ.ofFun '' {x : ℕ → ℝ | ∀ᶠ (n : ℕ) in ↑(Filter.hyperfilter ℕ), x n ∈ E n}

@[reducible, inline]

abbrev is_internal (E : Set ℝ*) : Prop

Equations

• is_internal E = ∃ (E' : ℕ → Set ℝ), E = internal E'

theorem mem_internal (x : ℕ → ℝ) (E : ℕ → Set ℝ) : to_hyperreal x ∈ internal E ↔ ∀ᶠ (n : ℕ) in ↑(Filter.hyperfilter ℕ), x n ∈ E n

theorem saturation (I : ℕ → Set ℝ*) (hI : ∀ (n : ℕ), is_internal (I n)) (hI' : ∀ (n : ℕ), (I n).Nonempty) (hI'' : ∀ (n : ℕ), I (n + 1) ⊆ I n) : ∃ (x : ℝ*), ∀ (n : ℕ), x ∈ I n

theorem Hyperreal.Ioi_internal (a b : ℝ*) : ∃ (E : ℕ → ℕ → Set ℝ), Set.Ioo a b = ⋂ (n : ℕ), internal (E n)

theorem Hyperreal.completeness (a b : ℕ → ℝ*) (ha : Monotone a) (hb : Antitone b) (hab : ∀ (n : ℕ), a n < b n) : ∃ (x : ℝ*), ∀ (n : ℕ), a n < x ∧ x < b n