mathlib documentation

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.

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
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
theorem real.zero_cauchy  :
0⟩ = 0
theorem real.one_cauchy  :
1⟩ = 1
theorem real.add_cauchy {a b : cau_seq.completion.Cauchy} :
a⟩ + b⟩ = a + b
theorem real.neg_cauchy {a : cau_seq.completion.Cauchy} :
-a⟩ = -a⟩
theorem real.mul_cauchy {a b : cau_seq.completion.Cauchy} :
a⟩ * b⟩ = a * b
@[instance]
Equations

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]
def real.ring  :
Equations
@[instance]
Equations
@[instance]
Equations
@[instance]

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

Equations

Coercion as a ring_hom. Note that this is cau_seq.completion.of_rat, not rat.cast.

Equations
def real.mk (x : cau_seq abs) :

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

Equations
theorem real.mk_eq {f g : cau_seq abs} :
@[instance]
Equations
theorem real.lt_cauchy {f g : cau_seq abs} :
f< g f < g
@[simp]
theorem real.mk_lt {f g : cau_seq abs} :
theorem real.mk_zero  :
theorem real.mk_one  :
theorem real.mk_add {f g : cau_seq abs} :
theorem real.mk_mul {f g : cau_seq abs} :
real.mk (f * g) = (real.mk f) * real.mk g
theorem real.mk_neg {f : cau_seq abs} :
@[simp]
theorem real.mk_pos {f : cau_seq abs} :
@[instance]
Equations
@[simp]
theorem real.mk_le {f g : cau_seq abs} :
theorem real.ind_mk {C : → Prop} (x : ) (h : ∀ (y : cau_seq abs), C (real.mk y)) :
C x
theorem real.add_lt_add_iff_left {a b : } (c : ) :
c + a < c + b a < b
@[instance]
Equations
theorem real.zero_lt_one  :
0 < 1
theorem real.mul_pos {a b : } :
0 < a0 < b0 < a * b
@[instance]
@[instance]
Equations
@[instance]

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

Equations
@[instance]
Equations
theorem real.inv_cauchy {f : cau_seq.completion.Cauchy} :
f⟩⁻¹ = f⁻¹
@[instance]
Equations
@[instance]
def real.decidable_lt (a b : ) :
decidable (a < b)
Equations
@[instance]
def real.decidable_le (a b : ) :
Equations
@[instance]
def real.decidable_eq (a b : ) :
decidable (a = b)
Equations
@[simp]
theorem real.le_mk_of_forall_le {x : } {f : cau_seq abs} :
(∃ (i : ), ∀ (j : ), j ix (f j))x real.mk f
theorem real.mk_le_of_forall_le {f : cau_seq abs} {x : } (h : ∃ (i : ), ∀ (j : ), j i(f j) x) :
theorem real.mk_near_of_forall_near {f : cau_seq abs} {x ε : } (H : ∃ (i : ), ∀ (j : ), j i|(f j) - x| ε) :
|real.mk f - x| ε
@[instance]
theorem real.is_cau_seq_iff_lift {f : } :
is_cau_seq abs f is_cau_seq abs (λ (i : ), (f i))
theorem real.of_near (f : ) (x : ) (h : ∀ (ε : ), ε > 0(∃ (i : ), ∀ (j : ), j i|(f j) - x| < ε)) :
∃ (h' : is_cau_seq abs f), 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 : ), is_lub S x
@[instance]
Equations
theorem real.Sup_def (S : set ) :
Sup S = dite (S.nonempty bdd_above S) (λ (h : S.nonempty bdd_above S), classical.some _) (λ (h : ¬(S.nonempty bdd_above S)), 0)
theorem real.is_lub_Sup (S : set ) (h₁ : S.nonempty) (h₂ : bdd_above S) :
is_lub S (Sup S)
@[instance]
Equations
theorem real.Inf_def (S : set ) :
Inf S = -Sup (-S)
theorem real.is_glb_Inf (S : set ) (h₁ : S.nonempty) (h₂ : bdd_below S) :
is_glb S (Inf S)
theorem real.lt_Inf_add_pos {s : set } (h : s.nonempty) {ε : } (hε : 0 < ε) :
∃ (a : ) (H : a s), a < Inf s + ε
theorem real.add_neg_lt_Sup {s : set } (h : s.nonempty) {ε : } (hε : ε < 0) :
∃ (a : ) (H : a s), Sup s + ε < a
theorem real.Inf_le_iff {s : set } (h : bdd_below s) (h' : s.nonempty) {a : } :
Inf s a ∀ (ε : ), 0 < ε(∃ (x : ) (H : x s), x < a + ε)
theorem real.le_Sup_iff {s : set } (h : bdd_above s) (h' : s.nonempty) {a : } :
a Sup s ∀ (ε : ), ε < 0(∃ (x : ) (H : x s), a + ε < x)
@[simp]
theorem real.Sup_empty  :
theorem real.Sup_of_not_bdd_above {s : set } (hs : ¬bdd_above s) :
Sup s = 0
@[simp]
theorem real.Inf_empty  :
theorem real.Inf_of_not_bdd_below {s : set } (hs : ¬bdd_below s) :
Inf s = 0
theorem real.Sup_nonneg (S : set ) (hS : ∀ (x : ), x S0 x) :
0 Sup S

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) :
Sup S 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 Inf S

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) :
Inf S 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) :
Inf s Sup s
theorem real.cau_seq_converges (f : cau_seq abs) :
∃ (x : ), f cau_seq.const abs x