# Real numbers from Cauchy sequences #

This file defines ℝ as the type of equivalence classes of Cauchy sequences of rational numbers. This choice is motivated by how easy it is to prove that ℝ is a commutative ring, by simply lifting everything to ℚ.

The facts that the real numbers are an Archimedean floor ring, and a conditionally complete linear order, have been deferred to the file Mathlib/Data/Real/Archimedean.lean, in order to keep the imports here simple.

structure Real :

The type ℝ of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.

• ofCauchy :: (
• cauchy :

The underlying Cauchy completion

• )
Instances For

The type ℝ of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.

Equations
Instances For
@[simp]
theorem CauSeq.Completion.ofRat_rat {abv : } [] (q : ) :
theorem Real.ext_cauchy_iff {x : } {y : } :
x = y x.cauchy = y.cauchy
theorem Real.ext_cauchy {x : } {y : } :
x.cauchy = y.cauchyx = y

The real numbers are isomorphic to the quotient of Cauchy sequences on the rationals.

Equations
Instances For
instance Real.instZero :
Equations
instance Real.instOne :
Equations
Equations
instance Real.instNeg :
Equations
instance Real.instMul :
Equations
instance Real.instSub :
Equations
noncomputable instance Real.instInv :
Equations
theorem Real.ofCauchy_zero :
{ cauchy := 0 } = 0
theorem Real.ofCauchy_one :
{ cauchy := 1 } = 1
theorem Real.ofCauchy_add (a : ) (b : ) :
{ cauchy := a + b } = { cauchy := a } + { cauchy := b }
theorem Real.ofCauchy_neg (a : ) :
{ cauchy := -a } = -{ cauchy := a }
theorem Real.ofCauchy_sub (a : ) (b : ) :
{ cauchy := a - b } = { cauchy := a } - { cauchy := b }
theorem Real.ofCauchy_mul (a : ) (b : ) :
{ cauchy := a * b } = { cauchy := a } * { cauchy := b }
theorem Real.ofCauchy_inv {f : } :
{ cauchy := f⁻¹ } = { cauchy := f }⁻¹
theorem Real.cauchy_add (a : ) (b : ) :
(a + b).cauchy = a.cauchy + b.cauchy
theorem Real.cauchy_neg (a : ) :
(-a).cauchy = -a.cauchy
theorem Real.cauchy_mul (a : ) (b : ) :
(a * b).cauchy = a.cauchy * b.cauchy
theorem Real.cauchy_sub (a : ) (b : ) :
(a - b).cauchy = a.cauchy - b.cauchy
theorem Real.cauchy_inv (f : ) :
f⁻¹.cauchy = f.cauchy⁻¹
instance Real.instNatCast :
Equations
instance Real.instIntCast :
Equations
Equations
instance Real.instRatCast :
Equations
theorem Real.ofCauchy_natCast (n : ) :
{ cauchy := n } = n
theorem Real.ofCauchy_intCast (z : ) :
{ cauchy := z } = z
theorem Real.ofCauchy_nnratCast (q : ℚ≥0) :
{ cauchy := q } = q
theorem Real.ofCauchy_ratCast (q : ) :
{ cauchy := q } = q
theorem Real.cauchy_natCast (n : ) :
(n).cauchy = n
theorem Real.cauchy_intCast (z : ) :
(z).cauchy = z
theorem Real.cauchy_nnratCast (q : ℚ≥0) :
(q).cauchy = q
theorem Real.cauchy_ratCast (q : ) :
(q).cauchy = q
instance Real.commRing :
Equations
@[simp]
theorem Real.ringEquivCauchy_symm_apply_cauchy (cauchy : ) :
(Real.ringEquivCauchy.symm cauchy).cauchy = cauchy
@[simp]
theorem Real.ringEquivCauchy_apply (self : ) :
Real.ringEquivCauchy self = self.cauchy

Real.equivCauchy as a ring equivalence.

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

Extra instances to short-circuit type class resolution.

These short-circuits have an additional property of ensuring that a computable path is found; if Field ℝ is found first, then decaying it to these typeclasses would result in a noncomputable version of them.

instance Real.instRing :
Equations
Equations
instance Real.semiring :
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
instance Real.instMonoid :
Equations
Equations
Equations
Equations

The real numbers are a *-ring, with the trivial *-structure.

Equations
Equations
def Real.mk (x : CauSeq abs) :

Make a real number from a Cauchy sequence of rationals (by taking the equivalence class).

Equations
• = { cauchy := }
Instances For
theorem Real.mk_eq {f : CauSeq abs} {g : CauSeq abs} :
= f g
instance Real.instLT :
Equations
theorem Real.lt_cauchy {f : CauSeq abs} {g : CauSeq abs} :
{ cauchy := f } < { cauchy := g } f < g
@[simp]
theorem Real.mk_lt {f : CauSeq abs} {g : CauSeq abs} :
< f < g
theorem Real.mk_zero :
= 0
theorem Real.mk_one :
= 1
theorem Real.mk_add {f : CauSeq abs} {g : CauSeq abs} :
Real.mk (f + g) = +
theorem Real.mk_mul {f : CauSeq abs} {g : CauSeq abs} :
Real.mk (f * g) = *
theorem Real.mk_neg {f : CauSeq abs} :
@[simp]
theorem Real.mk_pos {f : CauSeq abs} :
0 < f.Pos
instance Real.instLE :
Equations
@[simp]
theorem Real.mk_le {f : CauSeq abs} {g : CauSeq abs} :
f g
theorem Real.ind_mk {C : } (x : ) (h : ∀ (y : CauSeq abs), C ()) :
C x
theorem Real.add_lt_add_iff_left {a : } {b : } (c : ) :
c + a < c + b a < b
Equations
Equations
theorem Real.ratCast_lt {x : } {y : } :
x < y x < y
theorem Real.mul_pos {a : } {b : } :
0 < a0 < b0 < a * b
Equations
Equations
Equations
instance Real.orderedRing :
Equations
Equations
Equations
Equations
instance Real.nontrivial :
Equations
instance Real.instSup :
Equations
theorem Real.ofCauchy_sup (a : CauSeq abs) (b : CauSeq abs) :
{ cauchy := a b } = { cauchy := a } { cauchy := b }
@[simp]
theorem Real.mk_sup (a : CauSeq abs) (b : CauSeq abs) :
Real.mk (a b) =
instance Real.instInf :
Equations
theorem Real.ofCauchy_inf (a : CauSeq abs) (b : CauSeq abs) :
{ cauchy := a b } = { cauchy := a } { cauchy := b }
@[simp]
theorem Real.mk_inf (a : CauSeq abs) (b : CauSeq abs) :
Real.mk (a b) =
Equations
instance Real.lattice :
Equations
instance Real.instIsTotalLe :
IsTotal fun (x x_1 : ) => x x_1
Equations
noncomputable instance Real.linearOrder :
Equations
noncomputable instance Real.linearOrderedCommRing :
Equations
noncomputable instance Real.instLinearOrderedRing :
Equations
noncomputable instance Real.instLinearOrderedSemiring :
Equations
Equations
noncomputable instance Real.instDivInvMonoid :
Equations
theorem Real.ofCauchy_div (f : ) (g : ) :
{ cauchy := f / g } = { cauchy := f } / { cauchy := g }
noncomputable instance Real.instLinearOrderedField :
Equations
• One or more equations did not get rendered due to their size.
noncomputable instance Real.field :
Equations
noncomputable instance Real.instDivisionRing :
Equations
noncomputable instance Real.decidableLT (a : ) (b : ) :
Decidable (a < b)
Equations
• a.decidableLT b = inferInstance
noncomputable instance Real.decidableLE (a : ) (b : ) :
Equations
• a.decidableLE b = inferInstance
noncomputable instance Real.decidableEq (a : ) (b : ) :
Decidable (a = b)
Equations
• a.decidableEq b = inferInstance
unsafe instance Real.instRepr :

Show an underlying cauchy sequence for real numbers.

The representative chosen is the one passed in the VM to Quot.mk, so two cauchy sequences converging to the same number may be printed differently.

Equations
theorem Real.le_mk_of_forall_le {x : } {f : CauSeq abs} :
(∃ (i : ), ji, x (f j))x
theorem Real.mk_le_of_forall_le {f : CauSeq abs} {x : } (h : ∃ (i : ), ji, (f j) x) :
x
theorem Real.mk_near_of_forall_near {f : CauSeq abs} {x : } {ε : } (H : ∃ (i : ), ji, |(f j) - x| ε) :
| - x| ε
def IsNonarchimedean {A : Type u_1} [Add A] (f : A) :

A function f : R → ℝ≥0 is nonarchimedean if it satisfies the strong triangle inequality f (r + s) ≤ max (f r) (f s) for all r s : R.

Equations
• = ∀ (r s : A), f (r + s) max (f r) (f s)
Instances For