The quotient field of interval-Cauchy sequences

Computableℝ is the quotient of ComputableℝSeq by the equivalence relation of converging to the same real value. This file equips it with its commutative ring, field, and linear order structures. The ring operations are executable interval arithmetic; inversion and the comparison Decidable instances go through the classical ComputableℝSeq.sign and are noncomputable.

def Computableℝ : Type

Computable reals, defined as the quotient of ComputableℝSeq sequences -- sequences with Cauchy sequences of lower and upper bounds that converge to the same value -- by the equivalence relation of having the same converged value. This is similar to how reals are quotients of Cauchy sequence (without any guarantees on lower/upper bounds).

Equations

• Computableℝ = Quotient ComputableℝSeq.equiv

def Computableℝ.mk : ComputableℝSeq → Computableℝ

Definition of mk.

Equations

• Computableℝ.mk = Quotient.mk ComputableℝSeq.equiv

def Computableℝ.val : Computableℝ → ℝ

Definition of val.

Equations

• Computableℝ.val = Quotient.lift ComputableℝSeq.val ⋯

@[simp]

theorem Computableℝ.val_mk_eq_val {x : ComputableℝSeq} : (mk x).val = x.val

@[simp]

theorem Computableℝ.val_quot_eq_val (x : ComputableℝSeq) : val ⟦x⟧ = x.val

theorem Computableℝ.eq_iff_seq_val (x y : ComputableℝSeq) : (mk x).val = (mk y).val ↔ mk x = mk y

@[simp]

theorem Computableℝ.eq_iff_eq_val (x y : Computableℝ) : x.val = y.val ↔ x = y

def Computableℝ.mapℝ' (f : ComputableℝSeq → ComputableℝSeq) (h : ∃ (f₂ : ℝ → ℝ), ∀ (x : ComputableℝSeq), (f x).val = f₂ x.val) : Computableℝ → Computableℝ

Alternate version of mapℝ that doesn't directly refer to f₂, so it stays computable even if f₂ isn't.

Equations

• Computableℝ.mapℝ' f h = Quotient.map f ⋯

def Computableℝ.mapℝ (f : ComputableℝSeq → ComputableℝSeq) {f₂ : ℝ → ℝ} (h : ∀ (x : ComputableℝSeq), (f x).val = f₂ x.val) : Computableℝ → Computableℝ

Given a unary function on sequences that clearly matches function on reals, lift it.

Equations

• Computableℝ.mapℝ f h = Computableℝ.mapℝ' f ⋯

theorem Computableℝ.mapℝ'_eq_mapℝ {f : ComputableℝSeq → ComputableℝSeq} {h : ∃ (f₂ : ℝ → ℝ), ∀ (x : ComputableℝSeq), (f x).val = f₂ x.val} {f₂✝ : ℝ → ℝ} {h₂ : ∀ (x : ComputableℝSeq), (f x).val = f₂✝ x.val} : mapℝ' f h = mapℝ f h₂

def Computableℝ.map₂ℝ' (f : ComputableℝSeq → ComputableℝSeq → ComputableℝSeq) (h : ∃ (f₂ : ℝ → ℝ → ℝ), ∀ (x y : ComputableℝSeq), (f x y).val = f₂ x.val y.val) : Computableℝ → Computableℝ → Computableℝ

Alternate version of map₂ℝ that doesn't directly refer to f₂, so it stays computable even if f₂ isn't.

Equations

• Computableℝ.map₂ℝ' f h = Quotient.map₂ f ⋯

def Computableℝ.map₂ℝ (f : ComputableℝSeq → ComputableℝSeq → ComputableℝSeq) {f₂ : ℝ → ℝ → ℝ} (h : ∀ (x y : ComputableℝSeq), (f x y).val = f₂ x.val y.val) : Computableℝ → Computableℝ → Computableℝ

Given a binary function that clearly mimics a standard real function, lift that.

Equations

• Computableℝ.map₂ℝ f h = Computableℝ.map₂ℝ' f ⋯

theorem Computableℝ.map₂ℝ'_eq_map₂ℝ {f : ComputableℝSeq → ComputableℝSeq → ComputableℝSeq} {h : ∃ (f₂ : ℝ → ℝ → ℝ), ∀ (x y : ComputableℝSeq), (f x y).val = f₂ x.val y.val} {f₂✝ : ℝ → ℝ → ℝ} {h₂ : ∀ (x y : ComputableℝSeq), (f x y).val = f₂✝ x.val y.val} : map₂ℝ' f h = map₂ℝ f h₂

@[simp]

theorem Computableℝ.val_mapℝ_eq_val {f : ComputableℝSeq → ComputableℝSeq} {f₂ : ℝ → ℝ} {h : ∀ (x : ComputableℝSeq), (f x).val = f₂ x.val} {x : Computableℝ} : (mapℝ f h x).val = f₂ x.val

@[simp]

theorem Computableℝ.val_map₂ℝ_eq_val {f : ComputableℝSeq → ComputableℝSeq → ComputableℝSeq} {f₂ : ℝ → ℝ → ℝ} {h : ∀ (x y : ComputableℝSeq), (f x y).val = f₂ x.val y.val} {x y : Computableℝ} : (map₂ℝ f h x y).val = f₂ x.val y.val

@[instance_reducible]

instance Computableℝ.instComputableAdd : Add Computableℝ

Equations

• Computableℝ.instComputableAdd = { add := Computableℝ.map₂ℝ (fun (x1 x2 : ComputableℝSeq) => x1 + x2) ComputableℝSeq.val_add }

@[instance_reducible]

instance Computableℝ.instComputableMul : Mul Computableℝ

Equations

• Computableℝ.instComputableMul = { mul := Computableℝ.map₂ℝ (fun (x1 x2 : ComputableℝSeq) => x1 * x2) ComputableℝSeq.val_mul }

@[instance_reducible]

instance Computableℝ.instComputableNeg : Neg Computableℝ

Equations

• Computableℝ.instComputableNeg = { neg := Computableℝ.mapℝ (fun (x : ComputableℝSeq) => -x) ComputableℝSeq.val_neg }

@[instance_reducible]

instance Computableℝ.instComputableSub : Sub Computableℝ

Equations

• Computableℝ.instComputableSub = { sub := Computableℝ.map₂ℝ (fun (x1 x2 : ComputableℝSeq) => x1 - x2) ComputableℝSeq.val_sub }

@[instance_reducible]

instance Computableℝ.instComputableZero : Zero Computableℝ

Equations

• Computableℝ.instComputableZero = { zero := Computableℝ.mk 0 }

@[instance_reducible]

instance Computableℝ.instComputableOne : One Computableℝ

Equations

• Computableℝ.instComputableOne = { one := Computableℝ.mk 1 }

@[simp]

theorem Computableℝ.val_add (x y : Computableℝ) : (x + y).val = x.val + y.val

@[simp]

theorem Computableℝ.val_mul (x y : Computableℝ) : (x * y).val = x.val * y.val

@[simp]

theorem Computableℝ.val_neg (x : Computableℝ) : (-x).val = -x.val

@[simp]

theorem Computableℝ.val_sub (x y : Computableℝ) : (x - y).val = x.val - y.val

@[simp]

theorem Computableℝ.val_zero : val 0 = 0

@[simp]

theorem Computableℝ.val_one : val 1 = 1

theorem Computableℝ.add_mk (x y : ComputableℝSeq) : mk x + mk y = mk (x + y)

theorem Computableℝ.mul_mk (x y : ComputableℝSeq) : mk x * mk y = mk (x * y)

theorem Computableℝ.sub_mk (x y : ComputableℝSeq) : mk x - mk y = mk (x - y)

theorem Computableℝ.neg_mk (x : ComputableℝSeq) : -mk x = mk (-x)

@[instance_reducible]

instance Computableℝ.instCommRing : CommRing Computableℝ

Equations

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

@[simp]

theorem Computableℝ.val_natpow (x : Computableℝ) (n : ℕ) : (x ^ n).val = x.val ^ n

theorem Computableℝ.val_nsmul (x : Computableℝ) (n : ℕ) : (n • x).val = n • x.val

def Computableℝ.nzQuotEquiv : { x : Quotient ComputableℝSeq.equiv // x ≠ 0 } ≃ Quotient (Subtype.instSetoid_mathlib fun (x : ComputableℝSeq) => x.val ≠ 0)

Identify nonzero computable reals with the quotient of their nonzero representatives.

Equations

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

noncomputable def Computableℝ.safeInv' : { x : Computableℝ // x ≠ 0 } → { x : Computableℝ // x ≠ 0 }

Auxiliary inverse definition that operates on the nonzero Computableℝ values.

Equations

• Computableℝ.safeInv' v = Computableℝ.nzQuotEquiv.invFun (Quotient.map ComputableℝSeq.invNz ⋯ (Computableℝ.nzQuotEquiv.toFun v))

theorem Computableℝ.safeInv_def (x : Computableℝ) (hnz : x ≠ 0) : x.safeInv hnz = ↑(safeInv' ⟨x, hnz⟩)

@[irreducible]

noncomputable def Computableℝ.safeInv (x : Computableℝ) (hnz : x ≠ 0) : Computableℝ

Inverse of a nonzero Computableℝ, safe (terminating) as long as x is nonzero.

Equations

• x.safeInv hnz = ↑(Computableℝ.safeInv' ⟨x, hnz⟩)

@[simp]

theorem Computableℝ.safeInv_val (x : Computableℝ) (hnz : x ≠ 0) : (x.safeInv hnz).val = x.val⁻¹

@[instance_reducible]

noncomputable instance Computableℝ.instComputableInv : Inv Computableℝ

Equations

• Computableℝ.instComputableInv = { inv := Computableℝ.mapℝ' (fun (x : ComputableℝSeq) => x⁻¹) Computableℝ.instComputableInv._proof_1 }

@[simp]

theorem Computableℝ.inv_val (x : Computableℝ) : x⁻¹.val = x.val⁻¹

@[instance_reducible]

noncomputable instance Computableℝ.instField : Field Computableℝ

Equations

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

@[simp]

theorem Computableℝ.div_val (x y : Computableℝ) : (x / y).val = x.val / y.val

def Computableℝ.lt (x y : Computableℝ) : Prop

Definition of lt.

Equations

• x.lt y = Quotient.lift (fun (z : ComputableℝSeq) => z.sign = SignType.pos) Computableℝ.lt._proof_1 (y - x)

@[instance_reducible]

instance Computableℝ.instLT : LT Computableℝ

Equations

• Computableℝ.instLT = { lt := Computableℝ.lt }

def Computableℝ.le (x y : Computableℝ) : Prop

Definition of le.

Equations

• x.le y = Quotient.lift (fun (z : ComputableℝSeq) => SignType.zero ≤ z.sign) Computableℝ.le._proof_1 (y - x)

@[instance_reducible]

instance Computableℝ.instLE : LE Computableℝ

Equations

• Computableℝ.instLE = { le := Computableℝ.le }

@[simp]

theorem Computableℝ.lt_iff_lt (x y : Computableℝ) : x.val < y.val ↔ x < y

@[simp]

theorem Computableℝ.le_iff_le (x y : Computableℝ) : x.val ≤ y.val ↔ x ≤ y

@[instance_reducible]

noncomputable instance Computableℝ.instDecidableLE : DecidableRel fun (x y : Computableℝ) => x ≤ y

Equations

• a.instDecidableLE b = id (⋯.mpr inferInstance)

@[instance_reducible]

noncomputable instance Computableℝ.instPartialOrder : PartialOrder Computableℝ

Equations

• Computableℝ.instPartialOrder = { le := fun (x1 x2 : Computableℝ) => x1 ≤ x2, lt := fun (x1 x2 : Computableℝ) => x1 < x2, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[instance_reducible]

noncomputable instance Computableℝ.instLinearOrder : LinearOrder Computableℝ

Equations

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

instance Computableℝ.instIsOrderedAddMonoid : IsOrderedAddMonoid Computableℝ

instance Computableℝ.instZeroLEOneClass : ZeroLEOneClass Computableℝ

instance Computableℝ.instIsStrictOrderedRing : IsStrictOrderedRing Computableℝ