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.

The fact that the real numbers are a (trivial) *-ring has similarly been deferred to Mathlib/Data/Real/Star.lean.

structure Real : Type

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

• ofCauchy :: (
• cauchy : CauSeq.Completion.Cauchy abs

  The underlying Cauchy completion

• )

def termℝ : Lean.ParserDescr

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

@[simp]

theorem CauSeq.Completion.ofRat_rat {abv : ℚ → ℚ} [IsAbsoluteValue abv] (q : ℚ) : ofRat q = ↑q

theorem Real.ext_cauchy_iff {x y : ℝ} : x = y ↔ x.cauchy = y.cauchy

theorem Real.ext_cauchy {x y : ℝ} : x.cauchy = y.cauchy → x = y

def Real.equivCauchy : ℝ ≃ CauSeq.Completion.Cauchy abs

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

instance Real.instZero : Zero ℝ

instance Real.instOne : One ℝ

instance Real.instAdd : Add ℝ

instance Real.instNeg : Neg ℝ

instance Real.instMul : Mul ℝ

instance Real.instSub : Sub ℝ

noncomputable instance Real.instInv : Inv ℝ

theorem Real.ofCauchy_zero : { cauchy := 0 } = 0

theorem Real.ofCauchy_one : { cauchy := 1 } = 1

theorem Real.ofCauchy_add (a b : CauSeq.Completion.Cauchy abs) : { cauchy := a + b } = { cauchy := a } + { cauchy := b }

theorem Real.ofCauchy_neg (a : CauSeq.Completion.Cauchy abs) : { cauchy := -a } = -{ cauchy := a }

theorem Real.ofCauchy_sub (a b : CauSeq.Completion.Cauchy abs) : { cauchy := a - b } = { cauchy := a } - { cauchy := b }

theorem Real.ofCauchy_mul (a b : CauSeq.Completion.Cauchy abs) : { cauchy := a * b } = { cauchy := a } * { cauchy := b }

theorem Real.ofCauchy_inv {f : CauSeq.Completion.Cauchy abs} : { cauchy := f⁻¹ } = { cauchy := f }⁻¹

theorem Real.cauchy_zero : cauchy 0 = 0

theorem Real.cauchy_one : cauchy 1 = 1

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 : NatCast ℝ

instance Real.instIntCast : IntCast ℝ

instance Real.instNNRatCast : NNRatCast ℝ

instance Real.instRatCast : RatCast ℝ

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 : CommRing ℝ

def Real.ringEquivCauchy : ℝ ≃+* CauSeq.Completion.Cauchy abs

Real.equivCauchy as a ring equivalence.

@[simp]

theorem Real.ringEquivCauchy_apply (self : ℝ) : ringEquivCauchy self = self.cauchy

@[simp]

theorem Real.ringEquivCauchy_symm_apply_cauchy (cauchy : CauSeq.Completion.Cauchy abs) : (ringEquivCauchy.symm cauchy).cauchy = cauchy

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 : Ring ℝ

instance Real.instCommSemiring : CommSemiring ℝ

instance Real.semiring : Semiring ℝ

instance Real.instCommMonoidWithZero : CommMonoidWithZero ℝ

instance Real.instMonoidWithZero : MonoidWithZero ℝ

instance Real.instAddCommGroup : AddCommGroup ℝ

instance Real.instAddGroup : AddGroup ℝ

instance Real.instAddCommMonoid : AddCommMonoid ℝ

instance Real.instAddMonoid : AddMonoid ℝ

instance Real.instAddLeftCancelSemigroup : AddLeftCancelSemigroup ℝ

instance Real.instAddRightCancelSemigroup : AddRightCancelSemigroup ℝ

instance Real.instAddCommSemigroup : AddCommSemigroup ℝ

instance Real.instAddSemigroup : AddSemigroup ℝ

instance Real.instCommMonoid : CommMonoid ℝ

instance Real.instMonoid : Monoid ℝ

instance Real.instCommSemigroup : CommSemigroup ℝ

instance Real.instSemigroup : Semigroup ℝ

instance Real.instInhabited : Inhabited ℝ

def Real.mk (x : CauSeq ℚ abs) : ℝ

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

theorem Real.mk_eq {f g : CauSeq ℚ abs} : mk f = mk g ↔ f ≈ g

instance Real.instLT : LT ℝ

theorem Real.lt_cauchy {f g : CauSeq ℚ abs} : { cauchy := ⟦f⟧ } < { cauchy := ⟦g⟧ } ↔ f < g

@[simp]

theorem Real.mk_lt {f g : CauSeq ℚ abs} : mk f < mk g ↔ f < g

theorem Real.mk_zero : mk 0 = 0

theorem Real.mk_one : mk 1 = 1

theorem Real.mk_add {f g : CauSeq ℚ abs} : mk (f + g) = mk f + mk g

theorem Real.mk_mul {f g : CauSeq ℚ abs} : mk (f * g) = mk f * mk g

theorem Real.mk_neg {f : CauSeq ℚ abs} : mk (-f) = -mk f

@[simp]

theorem Real.mk_pos {f : CauSeq ℚ abs} : 0 < mk f ↔ f.Pos

theorem Real.mk_const {x : ℚ} : mk (CauSeq.const abs x) = ↑x

instance Real.instLE : LE ℝ

@[simp]

theorem Real.mk_le {f g : CauSeq ℚ abs} : mk f ≤ mk g ↔ f ≤ g

theorem Real.ind_mk {C : ℝ → Prop} (x : ℝ) (h : ∀ (y : CauSeq ℚ abs), C (mk y)) : C x

theorem Real.add_lt_add_iff_left {a b : ℝ} (c : ℝ) : c + a < c + b ↔ a < b

instance Real.partialOrder : PartialOrder ℝ

instance Real.instPreorder : Preorder ℝ

theorem Real.ratCast_lt {x y : ℚ} : ↑x < ↑y ↔ x < y

theorem Real.zero_lt_one : 0 < 1

@[deprecated ZeroLEOneClass.factZeroLtOne (since := "2025-05-12")]

theorem Real.fact_zero_lt_one : Fact (0 < 1)

instance Real.instNontrivial : Nontrivial ℝ

instance Real.instZeroLEOneClass : ZeroLEOneClass ℝ

instance Real.instIsOrderedAddMonoid : IsOrderedAddMonoid ℝ

instance Real.instIsStrictOrderedRing : IsStrictOrderedRing ℝ

instance Real.instIsOrderedRing : IsOrderedRing ℝ

instance Real.instIsOrderedCancelAddMonoid : IsOrderedCancelAddMonoid ℝ

instance Real.instMax : Max ℝ

theorem Real.ofCauchy_sup (a b : CauSeq ℚ abs) : { cauchy := ⟦a ⊔ b⟧ } = max { cauchy := ⟦a⟧ } { cauchy := ⟦b⟧ }

@[simp]

theorem Real.mk_sup (a b : CauSeq ℚ abs) : mk (a ⊔ b) = max (mk a) (mk b)

instance Real.instMin : Min ℝ

theorem Real.ofCauchy_inf (a b : CauSeq ℚ abs) : { cauchy := ⟦a ⊓ b⟧ } = min { cauchy := ⟦a⟧ } { cauchy := ⟦b⟧ }

@[simp]

theorem Real.mk_inf (a b : CauSeq ℚ abs) : mk (a ⊓ b) = min (mk a) (mk b)

instance Real.instDistribLattice : DistribLattice ℝ

instance Real.lattice : Lattice ℝ

instance Real.instSemilatticeInf : SemilatticeInf ℝ

instance Real.instSemilatticeSup : SemilatticeSup ℝ

instance Real.leTotal_R : IsTotal ℝ fun (x1 x2 : ℝ) => x1 ≤ x2

noncomputable instance Real.linearOrder : LinearOrder ℝ

instance Real.instIsDomain : IsDomain ℝ

noncomputable instance Real.instDivInvMonoid : DivInvMonoid ℝ

theorem Real.ofCauchy_div (f g : CauSeq.Completion.Cauchy abs) : { cauchy := f / g } = { cauchy := f } / { cauchy := g }

noncomputable instance Real.field : Field ℝ

noncomputable instance Real.instDivisionRing : DivisionRing ℝ

noncomputable instance Real.decidableLT (a b : ℝ) : Decidable (a < b)

noncomputable instance Real.decidableLE (a b : ℝ) : Decidable (a ≤ b)

noncomputable instance Real.decidableEq (a b : ℝ) : Decidable (a = b)

unsafe instance Real.instRepr : Repr ℝ

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.

theorem Real.le_mk_of_forall_le {x : ℝ} {f : CauSeq ℚ abs} : (∃ (i : ℕ), ∀ j ≥ i, x ≤ ↑(↑f j)) → x ≤ mk f

theorem Real.mk_le_of_forall_le {f : CauSeq ℚ abs} {x : ℝ} (h : ∃ (i : ℕ), ∀ j ≥ i, ↑(↑f j) ≤ x) : mk f ≤ x

theorem Real.mk_near_of_forall_near {f : CauSeq ℚ abs} {x ε : ℝ} (H : ∃ (i : ℕ), ∀ j ≥ i, |↑(↑f j) - x| ≤ ε) : |mk f - x| ≤ ε

theorem Real.mul_add_one_le_add_one_pow {a : ℝ} (ha : 0 ≤ a) (b : ℕ) : a * ↑b + 1 ≤ (a + 1) ^ b

def IsPowMul {R : Type u_1} [Pow R ℕ] (f : R → ℝ) : Prop

A function f : R → ℝ is power-multiplicative if for all r ∈ R and all positive n ∈ ℕ, f (r ^ n) = (f r) ^ n.

theorem IsPowMul.map_one_le_one {R : Type u_1} [Monoid R] {f : R → ℝ} (hf : IsPowMul f) : f 1 ≤ 1

def RingHom.IsBoundedWrt {α : Type u_1} [Ring α] {β : Type u_2} [Ring β] (nα : α → ℝ) (nβ : β → ℝ) (f : α →+* β) : Prop

A ring homomorphism f : α →+* β is bounded with respect to the functions nα : α → ℝ and nβ : β → ℝ if there exists a positive constant C such that for all x in α, nβ (f x) ≤ C * nα x.