# Documentation

Mathlib.Data.Real.Basic

# 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 ℚ.

structure Real :
• ofCauchy :: (
• The underlying Cauchy completion

cauchy :
• )

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

Instances For

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

Equations
@[simp]
theorem CauSeq.Completion.ofRat_rat {abv : } [inst : ] (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
theorem Real.zero_def :
Real.zero = { cauchy := 0 }
theorem Real.one_def :
Real.one = { cauchy := 1 }
∀ (x x_1 : ), Real.add x x_1 = match x, x_1 with | { cauchy := a }, { cauchy := b } => { cauchy := a + b }
theorem Real.neg_def :
∀ (x : ), = match x with | { cauchy := a } => { cauchy := -a }
theorem Real.mul_def :
∀ (x x_1 : ), Real.mul x x_1 = match x, x_1 with | { cauchy := a }, { cauchy := b } => { cauchy := a * b }
instance Real.instSubReal :
Equations
noncomputable instance Real.instInvReal :
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_zero :
0.cauchy = 0
theorem Real.cauchy_one :
1.cauchy = 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.natCast :
Equations
instance Real.intCast :
Equations
instance Real.ratCast :
Equations
theorem Real.ofCauchy_natCast (n : ) :
{ cauchy := n } = n
theorem Real.ofCauchy_intCast (z : ) :
{ cauchy := z } = z
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_ratCast (q : ) :
(q).cauchy = q
instance Real.commRing :
Equations
@[simp]
theorem Real.ringEquivCauchy_symm_apply_cauchy (cauchy : ) :
(↑() cauchy).cauchy = cauchy
@[simp]
theorem Real.ringEquivCauchy_apply (self : ) :
Real.ringEquivCauchy self = self.cauchy

real.equiv_Cauchy as a ring equivalence.

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

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.

Equations
instance Real.semiring :
Equations
Equations
Equations
Equations

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

Equations
Equations
• One or more equations did not get rendered due to their size.
def Real.mk (x : CauSeq abs) :

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

Equations
• = { cauchy := }
theorem Real.mk_eq {f : CauSeq abs} {g : CauSeq abs} :
= f g
theorem Real.lt_def :
∀ (x x_1 : ), Real.lt x x_1 = match x, x_1 with | { cauchy := x }, { cauchy := y } => Quotient.liftOn₂ x y (fun x x_2 => x < x_2) Real.definition.proof_1✝
instance Real.instLTReal :
Equations
theorem Real.lt_cauchy {f : CauSeq abs} {g : CauSeq abs} :
{ cauchy := Quotient.mk CauSeq.equiv f } < { cauchy := Quotient.mk CauSeq.equiv g } f < g
@[simp]
theorem Real.mk_lt {f : CauSeq abs} {g : CauSeq abs} :
< f < g
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 <
theorem Real.le_def (x : ) (y : ) :
Real.le x y = (x < y x = y)
instance Real.instLEReal :
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
theorem Real.ratCast_lt {x : } {y : } :
x < y x < y
theorem Real.mul_pos {a : } {b : } :
0 < a0 < b0 < a * b
Equations
Equations
instance Real.orderedRing :
Equations
Equations
Equations
Equations
instance Real.nontrivial :
Equations
theorem Real.sup_def :
∀ (x x_1 : ), Real.sup x x_1 = match x, x_1 with | { cauchy := x }, { cauchy := y } => { cauchy := Quotient.map₂ (fun x x_2 => x x_2) Real.definition.proof_2✝ x y }
theorem Real.ofCauchy_sup (a : CauSeq abs) (b : CauSeq abs) :
{ cauchy := Quotient.mk CauSeq.equiv (a b) } = { cauchy := Quotient.mk CauSeq.equiv a } { cauchy := Quotient.mk CauSeq.equiv b }
@[simp]
theorem Real.mk_sup (a : CauSeq abs) (b : CauSeq abs) :
Real.mk (a b) =
theorem Real.inf_def :
∀ (x x_1 : ), Real.inf x x_1 = match x, x_1 with | { cauchy := x }, { cauchy := y } => { cauchy := Quotient.map₂ (fun x x_2 => x x_2) Real.definition.proof_2✝ x y }
theorem Real.ofCauchy_inf (a : CauSeq abs) (b : CauSeq abs) :
{ cauchy := Quotient.mk CauSeq.equiv (a b) } = { cauchy := Quotient.mk CauSeq.equiv a } { cauchy := Quotient.mk CauSeq.equiv b }
@[simp]
theorem Real.mk_inf (a : CauSeq abs) (b : CauSeq abs) :
Real.mk (a b) =
Equations
instance Real.lattice :
Equations
instance Real.instIsTotalRealLeInstLEReal :
IsTotal fun x x_1 => x x_1
Equations
noncomputable instance Real.linearOrder :
Equations
noncomputable instance Real.linearOrderedCommRing :
Equations
• One or more equations did not get rendered due to their size.
noncomputable instance Real.instLinearOrderedRingReal :
Equations
noncomputable instance Real.instLinearOrderedFieldReal :
Equations
• One or more equations did not get rendered due to their size.
noncomputable instance Real.field :
Equations
noncomputable instance Real.instDivisionRingReal :
Equations
noncomputable instance Real.decidableLT (a : ) (b : ) :
Decidable (a < b)
Equations
• = inferInstance
noncomputable instance Real.decidableLE (a : ) (b : ) :
Equations
• = inferInstance
noncomputable instance Real.decidableEq (a : ) (b : ) :
Decidable (a = b)
Equations
• = inferInstance
unsafe instance Real.instReprReal :

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, ∀ (j : ), j ix ↑(f j)) → x
theorem Real.mk_le_of_forall_le {f : CauSeq abs} {x : } (h : i, ∀ (j : ), j i↑(f j) x) :
x
theorem Real.mk_near_of_forall_near {f : CauSeq abs} {x : } {ε : } (H : i, ∀ (j : ), j iabs (↑(f j) - x) ε) :
abs ( - x) ε
theorem Real.isCauSeq_iff_lift {f : } :
IsCauSeq abs f IsCauSeq abs fun i => ↑(f i)
theorem Real.of_near (f : ) (x : ) (h : ∀ (ε : ), ε > 0i, ∀ (j : ), j iabs (↑(f j) - x) < ε) :
h', Real.mk { val := f, property := h' } = x
theorem Real.exists_floor (x : ) :
ub, ub x ∀ (z : ), z xz ub
theorem Real.exists_isLUB (S : ) (hne : ) (hbdd : ) :
x, IsLUB S x
noncomputable instance Real.instSupSetReal :
Equations
theorem Real.supₛ_def (S : ) :
supₛ S = if h : then Classical.choose (_ : x, IsLUB S x) else 0
theorem Real.isLUB_supₛ (S : ) (h₁ : ) (h₂ : ) :
noncomputable instance Real.instInfSetReal :
Equations
theorem Real.is_glb_infₛ (S : ) (h₁ : ) (h₂ : ) :
Equations
• One or more equations did not get rendered due to their size.
theorem Real.lt_infₛ_add_pos {s : } (h : ) {ε : } (hε : 0 < ε) :
a, a s a < infₛ s + ε
theorem Real.add_neg_lt_supₛ {s : } (h : ) {ε : } (hε : ε < 0) :
a, a s supₛ s + ε < a
theorem Real.infₛ_le_iff {s : } (h : ) (h' : ) {a : } :
infₛ s a ∀ (ε : ), 0 < εx, x s x < a + ε
theorem Real.le_supₛ_iff {s : } (h : ) (h' : ) {a : } :
a supₛ s ∀ (ε : ), ε < 0x, x s a + ε < x
@[simp]
theorem Real.supₛ_empty :
= 0
theorem Real.csupᵢ_empty {α : Sort u_1} [inst : ] (f : α) :
(i, f i) = 0
@[simp]
theorem Real.csupᵢ_const_zero {α : Sort u_1} :
(_i, 0) = 0
theorem Real.supₛ_of_not_bddAbove {s : } (hs : ) :
supₛ s = 0
theorem Real.supᵢ_of_not_bddAbove {α : Sort u_1} {f : α} (hf : ¬) :
(i, f i) = 0
theorem Real.supₛ_univ :
supₛ Set.univ = 0
@[simp]
theorem Real.infₛ_empty :
= 0
theorem Real.cinfᵢ_empty {α : Sort u_1} [inst : ] (f : α) :
(i, f i) = 0
@[simp]
theorem Real.cinfᵢ_const_zero {α : Sort u_1} :
(_i, 0) = 0
theorem Real.infₛ_of_not_bddBelow {s : } (hs : ) :
infₛ s = 0
theorem Real.infᵢ_of_not_bddBelow {α : Sort u_1} {f : α} (hf : ¬) :
(i, f i) = 0
theorem Real.supₛ_nonneg (S : ) (hS : ∀ (x : ), x S0 x) :

As 0 is the default value for Real.supₛ of the empty set or sets which are not bounded above, it suffices to show that S is bounded below by 0 to show that 0 ≤ infₛ S.

theorem Real.supₛ_nonpos (S : ) (hS : ∀ (x : ), x Sx 0) :

As 0 is the default value for Real.supₛ of the empty set, it suffices to show that S is bounded above by 0 to show that supₛ S ≤ 0.

theorem Real.infₛ_nonneg (S : ) (hS : ∀ (x : ), x S0 x) :

As 0 is the default value for Real.infₛ of the empty set, it suffices to show that S is bounded below by 0 to show that 0 ≤ infₛ S.

theorem Real.infᵢ_nonneg {ι : Sort u_1} {f : ι} (hf : ∀ (i : ι), 0 f i) :

As 0 is the default value for Real.infₛ of the empty set, it suffices to show that f i is bounded below by 0 to show that 0 ≤ infᵢ f.

theorem Real.infₛ_nonpos (S : ) (hS : ∀ (x : ), x Sx 0) :

As 0 is the default value for Real.infₛ of the empty set or sets which are not bounded below, it suffices to show that S is bounded above by 0 to show that infₛ S ≤ 0.

theorem Real.infₛ_le_supₛ (s : ) (h₁ : ) (h₂ : ) :
theorem Real.cauSeq_converges (f : CauSeq abs) :
x, f CauSeq.const abs x
Equations
• One or more equations did not get rendered due to their size.