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  :
Type

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

Instances for real
@[simp]
theorem cau_seq.completion.of_rat_rat {abv : } [is_absolute_value 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
@[protected, instance]
Equations
@[protected, instance]
def real.has_one  :
Equations
@[protected, instance]
Equations
@[protected, instance]
def real.has_neg  :
Equations
@[protected, instance]
def real.has_mul  :
Equations
@[protected, instance]
noncomputable def real.has_inv  :
Equations
theorem real.of_cauchy_zero  :
0⟩ = 0
theorem real.of_cauchy_one  :
1⟩ = 1
theorem real.of_cauchy_add (a b : cau_seq.completion.Cauchy) :
a + b = a⟩ + b⟩
theorem real.of_cauchy_neg  :
-a⟩ = -a⟩
theorem real.of_cauchy_mul (a b : cau_seq.completion.Cauchy) :
a * b = a⟩ * b⟩
theorem real.of_cauchy_inv  :
f⁻¹= 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 : ) :
theorem real.cauchy_mul (a b : ) :
(a * b).cauchy = a.cauchy * b.cauchy
@[simp]
theorem real.ring_equiv_Cauchy_apply (self : ) :
= self.cauchy

real.equiv_Cauchy as a ring equivalence.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem real.of_cauchy_nat_cast (n : ) :
n⟩ = n
theorem real.of_cauchy_int_cast (z : ) :
z⟩ = z
theorem real.of_cauchy_rat_cast (q : ) :
q⟩ = q

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.

@[protected, instance]
def real.ring  :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def real.monoid  :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def real.has_sub  :
Equations
@[protected, instance]
def real.module  :
Equations
@[protected, instance]
Equations
@[protected, instance]

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

Equations
@[protected, instance]
def real.mk (x : has_abs.abs) :

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

Equations
theorem real.mk_eq {f g : has_abs.abs} :
= f g
@[protected, instance]
def real.has_lt  :
Equations
theorem real.lt_cauchy {f g : has_abs.abs} :
f< g f < g
@[simp]
theorem real.mk_lt {f g : has_abs.abs} :
< f < g
theorem real.mk_zero  :
= 0
theorem real.mk_one  :
= 1
theorem real.mk_add {f g : has_abs.abs} :
real.mk (f + g) = +
theorem real.mk_mul {f g : has_abs.abs} :
real.mk (f * g) = *
theorem real.mk_neg {f : has_abs.abs} :
@[simp]
theorem real.mk_pos {f : has_abs.abs} :
0 < f.pos
@[protected, instance]
def real.has_le  :
Equations
@[simp]
theorem real.mk_le {f g : has_abs.abs} :
f g
@[protected]
theorem real.ind_mk {C : → Prop} (x : ) (h : ∀ (y : , C (real.mk y)) :
C x
c + a < c + b a < b
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem real.rat_cast_lt {x y : } :
x < y x < y
@[protected]
theorem real.zero_lt_one  :
0 < 1
@[protected]
theorem real.mul_pos {a b : } :
0 < a0 < b0 < a * b
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
noncomputable def real.linear_order  :
Equations
@[protected, instance]
noncomputable def real.linear_ordered_comm_ring  :
Equations
@[protected, instance]
noncomputable def real.linear_ordered_ring  :
Equations
@[protected, instance]
noncomputable def real.linear_ordered_semiring  :
Equations
@[protected, instance]
@[protected, instance]
noncomputable def real.linear_ordered_field  :
Equations
@[protected, instance]
Equations
@[protected, instance]
noncomputable def real.field  :
Equations
@[protected, instance]
noncomputable def real.division_ring  :
Equations
@[protected, instance]
noncomputable def real.distrib_lattice  :
Equations
@[protected, instance]
noncomputable def real.lattice  :
Equations
@[protected, instance]
noncomputable def real.semilattice_inf  :
Equations
@[protected, instance]
noncomputable def real.semilattice_sup  :
Equations
@[protected, instance]
noncomputable def real.has_inf  :
Equations
@[protected, instance]
noncomputable def real.has_sup  :
Equations
@[protected, instance]
noncomputable def real.decidable_lt (a b : ) :
decidable (a < b)
Equations
@[protected, instance]
noncomputable def real.decidable_le (a b : ) :
Equations
@[protected, instance]
noncomputable def real.decidable_eq (a b : ) :
decidable (a = b)
Equations
@[protected, instance]
meta def real.has_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 : has_abs.abs} :
(∃ (i : ), ∀ (j : ), j ix (f j))x
theorem real.mk_le_of_forall_le {f : has_abs.abs} {x : } (h : ∃ (i : ), ∀ (j : ), j i(f j) x) :
x
theorem real.mk_near_of_forall_near {f : has_abs.abs} {x ε : } (H : ∃ (i : ), ∀ (j : ), j i|(f j) - x| ε) :
| - x| ε
@[protected, instance]
@[protected, instance]
noncomputable def real.floor_ring  :
Equations
theorem real.is_cau_seq_iff_lift {f : } :
(λ (i : ), (f i))
theorem real.of_near (f : ) (x : ) (h : ∀ (ε : ), ε > 0(∃ (i : ), ∀ (j : ), j i|(f j) - x| < ε)) :
∃ (h' : , real.mk f, h'⟩ = x
theorem real.exists_floor (x : ) :
∃ (ub : ), ub x ∀ (z : ), z xz ub
theorem real.exists_is_lub (S : set ) (hne : S.nonempty) (hbdd : bdd_above S) :
∃ (x : ), x
@[protected, instance]
noncomputable def real.has_Sup  :
Equations
theorem real.Sup_def (S : set ) :
= dite (S.nonempty (λ (h : S.nonempty , (λ (h : ¬(S.nonempty bdd_above S)), 0)
@[protected]
theorem real.is_lub_Sup (S : set ) (h₁ : S.nonempty) (h₂ : bdd_above S) :
@[protected, instance]
noncomputable def real.has_Inf  :
Equations
theorem real.Inf_def (S : set ) :
@[protected]
theorem real.is_glb_Inf (S : set ) (h₁ : S.nonempty) (h₂ : bdd_below S) :
@[protected, instance]
Equations
theorem real.lt_Inf_add_pos {s : set } (h : s.nonempty) {ε : } (hε : 0 < ε) :
∃ (a : ) (H : a s), a < + ε
theorem real.add_neg_lt_Sup {s : set } (h : s.nonempty) {ε : } (hε : ε < 0) :
∃ (a : ) (H : a s), + ε < a
theorem real.Inf_le_iff {s : set } (h : bdd_below s) (h' : s.nonempty) {a : } :
a ∀ (ε : ), 0 < ε(∃ (x : ) (H : x s), x < a + ε)
theorem real.le_Sup_iff {s : set } (h : bdd_above s) (h' : s.nonempty) {a : } :
a ∀ (ε : ), ε < 0(∃ (x : ) (H : x s), a + ε < x)
@[simp]
theorem real.Sup_empty  :
theorem real.csupr_empty {α : Sort u_1} [is_empty α] (f : α → ) :
(⨆ (i : α), f i) = 0
@[simp]
theorem real.csupr_const_zero {α : Sort u_1} :
(⨆ (i : α), 0) = 0
theorem real.Sup_of_not_bdd_above {s : set } (hs : ¬) :
= 0
theorem real.supr_of_not_bdd_above {α : Sort u_1} {f : α → } (hf : ¬) :
(⨆ (i : α), f i) = 0
theorem real.Sup_univ  :
@[simp]
theorem real.Inf_empty  :
theorem real.cinfi_empty {α : Sort u_1} [is_empty α] (f : α → ) :
(⨅ (i : α), f i) = 0
@[simp]
theorem real.cinfi_const_zero {α : Sort u_1} :
(⨅ (i : α), 0) = 0
theorem real.Inf_of_not_bdd_below {s : set } (hs : ¬) :
= 0
theorem real.infi_of_not_bdd_below {α : Sort u_1} {f : α → } (hf : ¬) :
(⨅ (i : α), f i) = 0
theorem real.Sup_nonneg (S : set ) (hS : ∀ (x : ), x S0 x) :
0

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 : set ) (hS : ∀ (x : ), x Sx 0) :
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 : set ) (hS : ∀ (x : ), x S0 x) :
0

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_nonpos (S : set ) (hS : ∀ (x : ), x Sx 0) :
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 : set ) (h₁ : bdd_below s) (h₂ : bdd_above s) :
theorem real.cau_seq_converges (f : has_abs.abs) :
∃ (x : ),
@[protected, instance]