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.

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

structure Real :

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
    Instances For
      @[simp]
      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
      Instances For
        Equations
        instance Real.instOne :
        Equations
        instance Real.instAdd :
        Equations
        instance Real.instNeg :
        Equations
        instance Real.instMul :
        Equations
        instance Real.instSub :
        Equations
        noncomputable instance Real.instInv :
        Equations
        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_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⁻¹
        Equations
        Equations
        Equations
        Equations
        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
        @[simp]
        theorem Real.ringEquivCauchy_apply (self : ) :
        Real.ringEquivCauchy self = self.cauchy
        @[simp]

        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.

          Equations
          Equations
          Equations
          Equations
          Equations
          def Real.mk (x : CauSeq abs) :

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

          Equations
          Instances For
            theorem Real.mk_eq {f : CauSeq abs} {g : CauSeq abs} :
            instance Real.instLT :
            Equations
            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} :
            theorem Real.mk_add {f : CauSeq abs} {g : CauSeq abs} :
            theorem Real.mk_mul {f : CauSeq abs} {g : CauSeq abs} :
            theorem Real.mk_neg {f : CauSeq abs} :
            @[simp]
            theorem Real.mk_pos {f : CauSeq abs} :
            0 < Real.mk f f.Pos
            instance Real.instLE :
            Equations
            @[simp]
            theorem Real.mk_le {f : CauSeq abs} {g : CauSeq abs} :
            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
            Equations
            theorem Real.ratCast_lt {x : } {y : } :
            x < y x < y
            @[deprecated mul_pos]
            theorem Real.mul_pos {a : } {b : } :
            0 < a0 < b0 < a * b
            Equations
            instance Real.instSup :
            Equations
            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) :
            instance Real.instInf :
            Equations
            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) :
            Equations
            instance Real.instIsTotalLe :
            IsTotal fun (x1 x2 : ) => x1 x2
            Equations
            theorem Real.ofCauchy_div (f : CauSeq.Completion.Cauchy abs) (g : CauSeq.Completion.Cauchy abs) :
            { cauchy := f / g } = { cauchy := f } / { cauchy := g }
            Equations
            • One or more equations did not get rendered due to their size.
            noncomputable instance Real.field :
            Equations
            noncomputable instance Real.instDivisionRing :
            Equations
            noncomputable instance Real.decidableLT (a : ) (b : ) :
            Decidable (a < b)
            Equations
            • a.decidableLT b = inferInstance
            noncomputable instance Real.decidableLE (a : ) (b : ) :
            Equations
            • a.decidableLE b = inferInstance
            noncomputable instance Real.decidableEq (a : ) (b : ) :
            Decidable (a = b)
            Equations
            • a.decidableEq b = inferInstance
            unsafe instance Real.instRepr :

            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 : ), ji, x (f j))x Real.mk f
            theorem Real.mk_le_of_forall_le {f : CauSeq abs} {x : } (h : ∃ (i : ), ji, (f j) x) :
            theorem Real.mk_near_of_forall_near {f : CauSeq abs} {x : } {ε : } (H : ∃ (i : ), ji, |(f j) - x| ε) :
            |Real.mk f - x| ε
            theorem Real.mul_add_one_le_add_one_pow {a : } (ha : 0 a) (b : ) :
            a * b + 1 (a + 1) ^ b
            def IsNonarchimedean {A : Type u_1} [Add A] (f : A) :

            A function f : R → ℝ≥0 is nonarchimedean if it satisfies the strong triangle inequality f (r + s) ≤ max (f r) (f s) for all r s : R.

            Equations
            Instances For
              def IsPowMul {R : Type u_1} [Pow R ] (f : R) :

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

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

                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.

                Equations
                Instances For