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

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 : CauSeq.Completion.Cauchy abs
The underlying Cauchy completion

)

Instances For

Lean.ParserDescr

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

Equations

termℝ = Lean.ParserDescr.node `termℝ 1024 (Lean.ParserDescr.symbol "ℝ")

Instances For

@[simp]

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

CauSeq.Completion.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.

Equations

Real.equivCauchy = { toFun := Real.cauchy, invFun := Real.ofCauchy, left_inv := Real.equivCauchy.proof_1, right_inv := Real.equivCauchy.proof_2 }

Instances For

instance Real.instZeroReal :

Equations

Real.instZeroReal = { zero := Real.zero }

instance Real.instOneReal :

Equations

Real.instOneReal = { one := Real.one }

instance Real.instAddReal :

Equations

Real.instAddReal = { add := Real.add }

instance Real.instNegReal :

Equations

Real.instNegReal = { neg := Real.neg }

instance Real.instMulReal :

Equations

Real.instMulReal = { mul := Real.mul }

instance Real.instSubReal :

Equations

Real.instSubReal = { sub := fun (a b : ℝ) => a + -b }

noncomputable instance Real.instInvReal :

Equations

Real.instInvReal = { inv := Real.inv' }

theorem Real.ofCauchy_zero :

{ cauchy := 0 } = 0

theorem Real.ofCauchy_one :

{ cauchy := 1 } = 1

theorem Real.ofCauchy_add (a : CauSeq.Completion.Cauchy abs) (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 : CauSeq.Completion.Cauchy abs) (b : CauSeq.Completion.Cauchy abs) :

{ cauchy := a - b } = { cauchy := a } - { cauchy := b }

theorem Real.ofCauchy_mul (a : CauSeq.Completion.Cauchy abs) (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 :

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.instNatCast :

Equations

Real.instNatCast = { natCast := fun (n : ℕ) => { cauchy := ↑n } }

instance Real.instIntCast :

Equations

Real.instIntCast = { intCast := fun (z : ℤ) => { cauchy := ↑z } }

instance Real.instRatCast :

Equations

Real.instRatCast = { ratCast := fun (q : ℚ) => { cauchy := ↑q } }

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

Real.commRing = CommRing.mk Real.commRing.proof_25

@[simp]

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

((RingEquiv.symm Real.ringEquivCauchy) cauchy).cauchy = cauchy

@[simp]

theorem Real.ringEquivCauchy_apply (self : ℝ) :

Real.ringEquivCauchy self = self.cauchy

def Real.ringEquivCauchy :

ℝ ≃+* CauSeq.Completion.Cauchy abs

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.instRingReal :

Equations

Real.instRingReal = inferInstance

instance Real.instCommSemiringReal :

CommSemiring ℝ

Equations

Real.instCommSemiringReal = inferInstance

instance Real.semiring :

Equations

Real.semiring = inferInstance

instance Real.instCommMonoidWithZeroReal :

CommMonoidWithZero ℝ

Equations

Real.instCommMonoidWithZeroReal = inferInstance

instance Real.instMonoidWithZeroReal :

MonoidWithZero ℝ

Equations

Real.instMonoidWithZeroReal = inferInstance

instance Real.instAddCommGroupReal :

AddCommGroup ℝ

Equations

Real.instAddCommGroupReal = inferInstance

instance Real.instAddGroupReal :

Equations

Real.instAddGroupReal = inferInstance

instance Real.instAddCommMonoidReal :

AddCommMonoid ℝ

Equations

Real.instAddCommMonoidReal = inferInstance

instance Real.instAddMonoidReal :

Equations

Real.instAddMonoidReal = inferInstance

instance Real.instAddLeftCancelSemigroupReal :

AddLeftCancelSemigroup ℝ

Equations

Real.instAddLeftCancelSemigroupReal = inferInstance

instance Real.instAddRightCancelSemigroupReal :

AddRightCancelSemigroup ℝ

Equations

Real.instAddRightCancelSemigroupReal = inferInstance

instance Real.instAddCommSemigroupReal :

AddCommSemigroup ℝ

Equations

Real.instAddCommSemigroupReal = inferInstance

instance Real.instAddSemigroupReal :

AddSemigroup ℝ

Equations

Real.instAddSemigroupReal = inferInstance

instance Real.instCommMonoidReal :

Equations

Real.instCommMonoidReal = inferInstance

instance Real.instMonoidReal :

Equations

Real.instMonoidReal = inferInstance

instance Real.instCommSemigroupReal :

CommSemigroup ℝ

Equations

Real.instCommSemigroupReal = inferInstance

instance Real.instSemigroupReal :

Equations

Real.instSemigroupReal = inferInstance

instance Real.instInhabitedReal :

Equations

Real.instInhabitedReal = { default := 0 }

instance Real.instStarRingRealToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingCommRing :

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

Equations

Real.instStarRingRealToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingCommRing = starRingOfComm

instance Real.instTrivialStarRealToStarToInvolutiveStarInstAddMonoidRealToStarAddMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingCommRingInstStarRingRealToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingCommRing :

TrivialStar ℝ

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

Real.mk x = { cauchy := CauSeq.Completion.mk x }

Instances For

theorem Real.mk_eq {f : CauSeq ℚ abs} {g : CauSeq ℚ abs} :

Real.mk f = Real.mk g ↔ f ≈ g

instance Real.instLTReal :

Equations

Real.instLTReal = { lt := Real.lt }

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

Real.mk f < Real.mk g ↔ f < g

theorem Real.mk_zero :

theorem Real.mk_one :

theorem Real.mk_add {f : CauSeq ℚ abs} {g : CauSeq ℚ abs} :

Real.mk (f + g) = Real.mk f + Real.mk g

theorem Real.mk_mul {f : CauSeq ℚ abs} {g : CauSeq ℚ abs} :

Real.mk (f * g) = Real.mk f * Real.mk g

theorem Real.mk_neg {f : CauSeq ℚ abs} :

Real.mk (-f) = -Real.mk f

@[simp]

theorem Real.mk_pos {f : CauSeq ℚ abs} :

0 < Real.mk f ↔ CauSeq.Pos f

instance Real.instLEReal :

Equations

Real.instLEReal = { le := Real.le }

@[simp]

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

Real.mk f ≤ Real.mk g ↔ f ≤ g

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

C x

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

c + a < c + b ↔ a < b

instance Real.partialOrder :

PartialOrder ℝ

Equations

Real.partialOrder = PartialOrder.mk Real.partialOrder.proof_4

instance Real.instPreorderReal :

Equations

Real.instPreorderReal = inferInstance

theorem Real.ratCast_lt {x : ℚ} {y : ℚ} :

↑x < ↑y ↔ x < y

theorem Real.zero_lt_one :

0 < 1

theorem Real.fact_zero_lt_one :

Fact (0 < 1)

theorem Real.mul_pos {a : ℝ} {b : ℝ} :

0 < a → 0 < b → 0 < a * b

instance Real.instStrictOrderedCommRingReal :

StrictOrderedCommRing ℝ

Equations

Real.instStrictOrderedCommRingReal = let __src := Real.commRing; let __src_1 := Real.partialOrder; let __src_2 := Real.semiring; StrictOrderedCommRing.mk ⋯

instance Real.strictOrderedRing :

StrictOrderedRing ℝ

Equations

Real.strictOrderedRing = inferInstance

instance Real.strictOrderedCommSemiring :

StrictOrderedCommSemiring ℝ

Equations

Real.strictOrderedCommSemiring = inferInstance

instance Real.strictOrderedSemiring :

StrictOrderedSemiring ℝ

Equations

Real.strictOrderedSemiring = inferInstance

instance Real.orderedRing :

OrderedRing ℝ

Equations

Real.orderedRing = inferInstance

instance Real.orderedSemiring :

OrderedSemiring ℝ

Equations

Real.orderedSemiring = inferInstance

instance Real.orderedAddCommGroup :

OrderedAddCommGroup ℝ

Equations

Real.orderedAddCommGroup = inferInstance

instance Real.orderedCancelAddCommMonoid :

OrderedCancelAddCommMonoid ℝ

Equations

Real.orderedCancelAddCommMonoid = inferInstance

instance Real.orderedAddCommMonoid :

OrderedAddCommMonoid ℝ

Equations

Real.orderedAddCommMonoid = inferInstance

instance Real.nontrivial :

Equations

Real.nontrivial = ⋯

instance Real.instSupReal :

Equations

Real.instSupReal = { sup := Real.sup }

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) = Real.mk a ⊔ Real.mk b

instance Real.instInfReal :

Equations

Real.instInfReal = { inf := Real.inf }

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) = Real.mk a ⊓ Real.mk b

instance Real.instDistribLatticeReal :

DistribLattice ℝ

Equations

Real.instDistribLatticeReal = let __src := Real.partialOrder; DistribLattice.mk Real.instDistribLatticeReal.proof_10

instance Real.lattice :

Equations

Real.lattice = inferInstance

instance Real.instSemilatticeInfReal :

SemilatticeInf ℝ

Equations

Real.instSemilatticeInfReal = inferInstance

instance Real.instSemilatticeSupReal :

SemilatticeSup ℝ

Equations

Real.instSemilatticeSupReal = inferInstance

instance Real.instIsTotalRealLeInstLEReal :

IsTotal ℝ fun (x x_1 : ℝ) => x ≤ x_1

Equations

Real.instIsTotalRealLeInstLEReal = ⋯

noncomputable instance Real.linearOrder :

LinearOrder ℝ

Equations

Real.linearOrder = Lattice.toLinearOrder ℝ

noncomputable instance Real.linearOrderedCommRing :

LinearOrderedCommRing ℝ

Equations

Real.linearOrderedCommRing = let __src := Real.nontrivial; let __src_1 := Real.strictOrderedRing; let __src_2 := Real.commRing; let __src_3 := Real.linearOrder; LinearOrderedCommRing.mk ⋯

noncomputable instance Real.instLinearOrderedRingReal :

LinearOrderedRing ℝ

Equations

Real.instLinearOrderedRingReal = inferInstance

noncomputable instance Real.instLinearOrderedSemiringReal :

LinearOrderedSemiring ℝ

Equations

Real.instLinearOrderedSemiringReal = inferInstance

instance Real.instIsDomainRealSemiring :

Equations

Real.instIsDomainRealSemiring = ⋯

noncomputable instance Real.instDivInvMonoid :

DivInvMonoid ℝ

Equations

Real.instDivInvMonoid = DivInvMonoid.mk Real.instDivInvMonoid.proof_1 zpowRec Real.instDivInvMonoid.proof_2 Real.instDivInvMonoid.proof_3 Real.instDivInvMonoid.proof_4

theorem Real.ofCauchy_div (f : CauSeq.Completion.Cauchy abs) (g : CauSeq.Completion.Cauchy abs) :

{ cauchy := f / g } = { cauchy := f } / { cauchy := g }

noncomputable instance Real.instLinearOrderedField :

LinearOrderedField ℝ

Equations

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

noncomputable instance Real.instLinearOrderedAddCommGroupReal :

LinearOrderedAddCommGroup ℝ

Equations

Real.instLinearOrderedAddCommGroupReal = inferInstance

noncomputable instance Real.field :

Equations

Real.field = inferInstance

noncomputable instance Real.instDivisionRingReal :

DivisionRing ℝ

Equations

Real.instDivisionRingReal = inferInstance

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

Decidable (a < b)

Equations

Real.decidableLT a b = inferInstance

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

Decidable (a ≤ b)

Equations

Real.decidableLE a b = inferInstance

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

Decidable (a = b)

Equations

Real.decidableEq a b = 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

Real.instReprReal = { reprPrec := fun (r : ℝ) (x : ℕ) => Std.Format.text "Real.ofCauchy " ++ repr r.cauchy }

theorem Real.le_mk_of_forall_le {x : ℝ} {f : CauSeq ℚ abs} :

(∃ (i : ℕ), ∀ j ≥ i, x ≤ ↑(↑f j)) → x ≤ Real.mk f

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

Real.mk f ≤ x

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

|Real.mk f - x| ≤ ε