Documentation

Mathlib.Algebra.Order.CauSeq.Basic

Cauchy sequences #

A basic theory of Cauchy sequences, used in the construction of the reals and p-adic numbers. Where applicable, lemmas that will be reused in other contexts have been stated in extra generality. There are other "versions" of Cauchyness in the library, in particular Cauchy filters in topology. This is a concrete implementation that is useful for simplicity and computability reasons.

Important definitions #

Tags #

sequence, cauchy, abs val, absolute value

theorem rat_add_continuous_lemma {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] (abv : βα) [IsAbsoluteValue abv] {ε : α} (ε0 : 0 < ε) :
δ > 0, ∀ {a₁ a₂ b₁ b₂ : β}, abv (a₁ - b₁) < δabv (a₂ - b₂) < δabv (a₁ + a₂ - (b₁ + b₂)) < ε
theorem rat_mul_continuous_lemma {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] (abv : βα) [IsAbsoluteValue abv] {ε K₁ K₂ : α} (ε0 : 0 < ε) :
δ > 0, ∀ {a₁ a₂ b₁ b₂ : β}, abv a₁ < K₁abv b₂ < K₂abv (a₁ - b₁) < δabv (a₂ - b₂) < δabv (a₁ * a₂ - b₁ * b₂) < ε
theorem rat_inv_continuous_lemma {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_3} [DivisionRing β] (abv : βα) [IsAbsoluteValue abv] {ε K : α} (ε0 : 0 < ε) (K0 : 0 < K) :
δ > 0, ∀ {a b : β}, K abv aK abv babv (a - b) < δabv (a⁻¹ - b⁻¹) < ε
def IsCauSeq {α : Type u_3} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_4} [Ring β] (abv : βα) (f : β) :

A sequence is Cauchy if the distance between its entries tends to zero.

Equations
    Instances For
      theorem IsCauSeq.cauchy₂ {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : β} (hf : IsCauSeq abv f) {ε : α} (ε0 : 0 < ε) :
      ∃ (i : ), ji, ki, abv (f j - f k) < ε
      theorem IsCauSeq.cauchy₃ {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : β} (hf : IsCauSeq abv f) {ε : α} (ε0 : 0 < ε) :
      ∃ (i : ), ji, kj, abv (f k - f j) < ε
      theorem IsCauSeq.bounded {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : β} (hf : IsCauSeq abv f) :
      ∃ (r : α), ∀ (i : ), abv (f i) < r
      theorem IsCauSeq.bounded' {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : β} (hf : IsCauSeq abv f) (x : α) :
      r > x, ∀ (i : ), abv (f i) < r
      theorem IsCauSeq.const {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (x : β) :
      IsCauSeq abv fun (x_1 : ) => x
      theorem IsCauSeq.add {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f g : β} (hf : IsCauSeq abv f) (hg : IsCauSeq abv g) :
      IsCauSeq abv (f + g)
      theorem IsCauSeq.mul {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f g : β} (hf : IsCauSeq abv f) (hg : IsCauSeq abv g) :
      IsCauSeq abv (f * g)
      @[simp]
      theorem isCauSeq_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : β} :
      IsCauSeq abv (-f) IsCauSeq abv f
      theorem IsCauSeq.of_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : β} :
      IsCauSeq abv (-f)IsCauSeq abv f

      Alias of the forward direction of isCauSeq_neg.

      theorem IsCauSeq.neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : β} :
      IsCauSeq abv fIsCauSeq abv (-f)

      Alias of the reverse direction of isCauSeq_neg.

      def CauSeq {α : Type u_3} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (β : Type u_4) [Ring β] (abv : βα) :
      Type u_4

      CauSeq β abv is the type of β-valued Cauchy sequences, with respect to the absolute value function abv.

      Equations
        Instances For
          instance CauSeq.instCoeFunForallNat {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} :
          CoeFun (CauSeq β abv) fun (x : CauSeq β abv) => β
          Equations
            theorem CauSeq.ext {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} {f g : CauSeq β abv} (h : ∀ (i : ), f i = g i) :
            f = g
            theorem CauSeq.ext_iff {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} {f g : CauSeq β abv} :
            f = g ∀ (i : ), f i = g i
            theorem CauSeq.isCauSeq {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} (f : CauSeq β abv) :
            IsCauSeq abv f
            theorem CauSeq.cauchy {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} (f : CauSeq β abv) {ε : α} :
            0 < ε∃ (i : ), ji, abv (f j - f i) < ε
            def CauSeq.ofEq {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} (f : CauSeq β abv) (g : β) (e : ∀ (i : ), f i = g i) :
            CauSeq β abv

            Given a Cauchy sequence f, create a Cauchy sequence from a sequence g with the same values as f.

            Equations
              Instances For
                theorem CauSeq.cauchy₂ {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) {ε : α} :
                0 < ε∃ (i : ), ji, ki, abv (f j - f k) < ε
                theorem CauSeq.cauchy₃ {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) {ε : α} :
                0 < ε∃ (i : ), ji, kj, abv (f k - f j) < ε
                theorem CauSeq.bounded {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) :
                ∃ (r : α), ∀ (i : ), abv (f i) < r
                theorem CauSeq.bounded' {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) (x : α) :
                r > x, ∀ (i : ), abv (f i) < r
                instance CauSeq.instAdd {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                Add (CauSeq β abv)
                Equations
                  @[simp]
                  theorem CauSeq.coe_add {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f g : CauSeq β abv) :
                  ↑(f + g) = f + g
                  @[simp]
                  theorem CauSeq.add_apply {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f g : CauSeq β abv) (i : ) :
                  ↑(f + g) i = f i + g i
                  def CauSeq.const {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] (abv : βα) [IsAbsoluteValue abv] (x : β) :
                  CauSeq β abv

                  The constant Cauchy sequence.

                  Equations
                    Instances For
                      @[simp]
                      theorem CauSeq.coe_const {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (x : β) :
                      (const abv x) = Function.const x
                      @[simp]
                      theorem CauSeq.const_apply {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (x : β) (i : ) :
                      (const abv x) i = x
                      theorem CauSeq.const_inj {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {x y : β} :
                      const abv x = const abv y x = y
                      instance CauSeq.instZero {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                      Zero (CauSeq β abv)
                      Equations
                        instance CauSeq.instOne {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                        One (CauSeq β abv)
                        Equations
                          instance CauSeq.instInhabited {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                          Inhabited (CauSeq β abv)
                          Equations
                            @[simp]
                            theorem CauSeq.coe_zero {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                            0 = 0
                            @[simp]
                            theorem CauSeq.coe_one {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                            1 = 1
                            @[simp]
                            theorem CauSeq.zero_apply {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (i : ) :
                            0 i = 0
                            @[simp]
                            theorem CauSeq.one_apply {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (i : ) :
                            1 i = 1
                            @[simp]
                            theorem CauSeq.const_zero {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                            const abv 0 = 0
                            @[simp]
                            theorem CauSeq.const_one {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                            const abv 1 = 1
                            theorem CauSeq.const_add {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (x y : β) :
                            const abv (x + y) = const abv x + const abv y
                            instance CauSeq.instMul {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                            Mul (CauSeq β abv)
                            Equations
                              @[simp]
                              theorem CauSeq.coe_mul {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f g : CauSeq β abv) :
                              ↑(f * g) = f * g
                              @[simp]
                              theorem CauSeq.mul_apply {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f g : CauSeq β abv) (i : ) :
                              ↑(f * g) i = f i * g i
                              theorem CauSeq.const_mul {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (x y : β) :
                              const abv (x * y) = const abv x * const abv y
                              instance CauSeq.instNeg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                              Neg (CauSeq β abv)
                              Equations
                                @[simp]
                                theorem CauSeq.coe_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) :
                                ↑(-f) = -f
                                @[simp]
                                theorem CauSeq.neg_apply {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) (i : ) :
                                ↑(-f) i = -f i
                                theorem CauSeq.const_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (x : β) :
                                const abv (-x) = -const abv x
                                instance CauSeq.instSub {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                                Sub (CauSeq β abv)
                                Equations
                                  @[simp]
                                  theorem CauSeq.coe_sub {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f g : CauSeq β abv) :
                                  ↑(f - g) = f - g
                                  @[simp]
                                  theorem CauSeq.sub_apply {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f g : CauSeq β abv) (i : ) :
                                  ↑(f - g) i = f i - g i
                                  theorem CauSeq.const_sub {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (x y : β) :
                                  const abv (x - y) = const abv x - const abv y
                                  instance CauSeq.instSMul {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {G : Type u_3} [SMul G β] [IsScalarTower G β β] :
                                  SMul G (CauSeq β abv)
                                  Equations
                                    @[simp]
                                    theorem CauSeq.coe_smul {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {G : Type u_3} [SMul G β] [IsScalarTower G β β] (a : G) (f : CauSeq β abv) :
                                    ↑(a f) = a f
                                    @[simp]
                                    theorem CauSeq.smul_apply {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {G : Type u_3} [SMul G β] [IsScalarTower G β β] (a : G) (f : CauSeq β abv) (i : ) :
                                    ↑(a f) i = a f i
                                    theorem CauSeq.const_smul {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {G : Type u_3} [SMul G β] [IsScalarTower G β β] (a : G) (x : β) :
                                    const abv (a x) = a const abv x
                                    instance CauSeq.instIsScalarTower {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {G : Type u_3} [SMul G β] [IsScalarTower G β β] :
                                    IsScalarTower G (CauSeq β abv) (CauSeq β abv)
                                    instance CauSeq.addGroup {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                                    AddGroup (CauSeq β abv)
                                    Equations
                                      instance CauSeq.instNatCast {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                                      NatCast (CauSeq β abv)
                                      Equations
                                        instance CauSeq.instIntCast {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                                        IntCast (CauSeq β abv)
                                        Equations
                                          instance CauSeq.addGroupWithOne {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                                          Equations
                                            instance CauSeq.instPowNat {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                                            Pow (CauSeq β abv)
                                            Equations
                                              @[simp]
                                              theorem CauSeq.coe_pow {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) (n : ) :
                                              ↑(f ^ n) = f ^ n
                                              @[simp]
                                              theorem CauSeq.pow_apply {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) (n i : ) :
                                              ↑(f ^ n) i = f i ^ n
                                              theorem CauSeq.const_pow {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (x : β) (n : ) :
                                              const abv (x ^ n) = const abv x ^ n
                                              instance CauSeq.ring {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                                              Ring (CauSeq β abv)
                                              Equations
                                                instance CauSeq.instCommRingOfIsAbsoluteValue {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_3} [CommRing β] {abv : βα} [IsAbsoluteValue abv] :
                                                CommRing (CauSeq β abv)
                                                Equations
                                                  def CauSeq.LimZero {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} (f : CauSeq β abv) :

                                                  LimZero f holds when f approaches 0.

                                                  Equations
                                                    Instances For
                                                      theorem CauSeq.add_limZero {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f g : CauSeq β abv} (hf : f.LimZero) (hg : g.LimZero) :
                                                      (f + g).LimZero
                                                      theorem CauSeq.mul_limZero_right {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) {g : CauSeq β abv} (hg : g.LimZero) :
                                                      (f * g).LimZero
                                                      theorem CauSeq.mul_limZero_left {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : CauSeq β abv} (g : CauSeq β abv) (hg : f.LimZero) :
                                                      (f * g).LimZero
                                                      theorem CauSeq.neg_limZero {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : CauSeq β abv} (hf : f.LimZero) :
                                                      theorem CauSeq.sub_limZero {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f g : CauSeq β abv} (hf : f.LimZero) (hg : g.LimZero) :
                                                      (f - g).LimZero
                                                      theorem CauSeq.limZero_sub_rev {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f g : CauSeq β abv} (hfg : (f - g).LimZero) :
                                                      (g - f).LimZero
                                                      theorem CauSeq.zero_limZero {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                                                      theorem CauSeq.const_limZero {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {x : β} :
                                                      (const abv x).LimZero x = 0
                                                      instance CauSeq.equiv {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                                                      Setoid (CauSeq β abv)
                                                      Equations
                                                        theorem CauSeq.add_equiv_add {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f1 f2 g1 g2 : CauSeq β abv} (hf : f1 f2) (hg : g1 g2) :
                                                        f1 + g1 f2 + g2
                                                        theorem CauSeq.neg_equiv_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f g : CauSeq β abv} (hf : f g) :
                                                        -f -g
                                                        theorem CauSeq.sub_equiv_sub {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f1 f2 g1 g2 : CauSeq β abv} (hf : f1 f2) (hg : g1 g2) :
                                                        f1 - g1 f2 - g2
                                                        theorem CauSeq.equiv_def₃ {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f g : CauSeq β abv} (h : f g) {ε : α} (ε0 : 0 < ε) :
                                                        ∃ (i : ), ji, kj, abv (f k - g j) < ε
                                                        theorem CauSeq.limZero_congr {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f g : CauSeq β abv} (h : f g) :
                                                        theorem CauSeq.abv_pos_of_not_limZero {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : CauSeq β abv} (hf : ¬f.LimZero) :
                                                        K > 0, ∃ (i : ), ji, K abv (f j)
                                                        theorem CauSeq.of_near {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : β) (g : CauSeq β abv) (h : ε > 0, ∃ (i : ), ji, abv (f j - g j) < ε) :
                                                        IsCauSeq abv f
                                                        theorem CauSeq.not_limZero_of_not_congr_zero {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : CauSeq β abv} (hf : ¬f 0) :
                                                        theorem CauSeq.mul_equiv_zero {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (g : CauSeq β abv) {f : CauSeq β abv} (hf : f 0) :
                                                        g * f 0
                                                        theorem CauSeq.mul_equiv_zero' {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (g : CauSeq β abv) {f : CauSeq β abv} (hf : f 0) :
                                                        f * g 0
                                                        theorem CauSeq.mul_not_equiv_zero {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f g : CauSeq β abv} (hf : ¬f 0) (hg : ¬g 0) :
                                                        ¬f * g 0
                                                        theorem CauSeq.const_equiv {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {x y : β} :
                                                        const abv x const abv y x = y
                                                        theorem CauSeq.mul_equiv_mul {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f1 f2 g1 g2 : CauSeq β abv} (hf : f1 f2) (hg : g1 g2) :
                                                        f1 * g1 f2 * g2
                                                        theorem CauSeq.smul_equiv_smul {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {G : Type u_3} [SMul G β] [IsScalarTower G β β] {f1 f2 : CauSeq β abv} (c : G) (hf : f1 f2) :
                                                        c f1 c f2
                                                        theorem CauSeq.pow_equiv_pow {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f1 f2 : CauSeq β abv} (hf : f1 f2) (n : ) :
                                                        f1 ^ n f2 ^ n
                                                        theorem CauSeq.one_not_equiv_zero {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Ring β] [IsDomain β] (abv : βα) [IsAbsoluteValue abv] :
                                                        ¬const abv 1 const abv 0
                                                        theorem CauSeq.inv_aux {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] {f : CauSeq β abv} (hf : ¬f.LimZero) (ε : α) :
                                                        ε > 0∃ (i : ), ji, abv ((f j)⁻¹ - (f i)⁻¹) < ε
                                                        def CauSeq.inv {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) (hf : ¬f.LimZero) :
                                                        CauSeq β abv

                                                        Given a Cauchy sequence f with nonzero limit, create a Cauchy sequence with values equal to the inverses of the values of f.

                                                        Equations
                                                          Instances For
                                                            @[simp]
                                                            theorem CauSeq.coe_inv {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] {f : CauSeq β abv} (hf : ¬f.LimZero) :
                                                            (f.inv hf) = (↑f)⁻¹
                                                            @[simp]
                                                            theorem CauSeq.inv_apply {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] {f : CauSeq β abv} (hf : ¬f.LimZero) (i : ) :
                                                            (f.inv hf) i = (f i)⁻¹
                                                            theorem CauSeq.inv_mul_cancel {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] {f : CauSeq β abv} (hf : ¬f.LimZero) :
                                                            f.inv hf * f 1
                                                            theorem CauSeq.mul_inv_cancel {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] {f : CauSeq β abv} (hf : ¬f.LimZero) :
                                                            f * f.inv hf 1
                                                            theorem CauSeq.const_inv {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] {x : β} (hx : x 0) :
                                                            const abv x⁻¹ = (const abv x).inv
                                                            def CauSeq.Pos {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (f : CauSeq α abs) :

                                                            The entries of a positive Cauchy sequence eventually have a positive lower bound.

                                                            Equations
                                                              Instances For
                                                                theorem CauSeq.const_pos {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {x : α} :
                                                                (const abs x).Pos 0 < x
                                                                theorem CauSeq.add_pos {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {f g : CauSeq α abs} :
                                                                f.Posg.Pos(f + g).Pos
                                                                theorem CauSeq.pos_add_limZero {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {f g : CauSeq α abs} :
                                                                f.Posg.LimZero(f + g).Pos
                                                                theorem CauSeq.mul_pos {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {f g : CauSeq α abs} :
                                                                f.Posg.Pos(f * g).Pos
                                                                theorem CauSeq.trichotomy {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (f : CauSeq α abs) :
                                                                instance CauSeq.instLTAbs {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] :
                                                                Equations
                                                                  instance CauSeq.instLEAbs {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] :
                                                                  Equations
                                                                    theorem CauSeq.lt_of_lt_of_eq {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {f g h : CauSeq α abs} (fg : f < g) (gh : g h) :
                                                                    f < h
                                                                    theorem CauSeq.lt_of_eq_of_lt {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {f g h : CauSeq α abs} (fg : f g) (gh : g < h) :
                                                                    f < h
                                                                    theorem CauSeq.lt_trans {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {f g h : CauSeq α abs} (fg : f < g) (gh : g < h) :
                                                                    f < h
                                                                    theorem CauSeq.lt_irrefl {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {f : CauSeq α abs} :
                                                                    ¬f < f
                                                                    theorem CauSeq.le_of_eq_of_le {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {f g h : CauSeq α abs} (hfg : f g) (hgh : g h) :
                                                                    f h
                                                                    theorem CauSeq.le_of_le_of_eq {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {f g h : CauSeq α abs} (hfg : f g) (hgh : g h) :
                                                                    f h
                                                                    Equations
                                                                      theorem CauSeq.le_antisymm {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {f g : CauSeq α abs} (fg : f g) (gf : g f) :
                                                                      f g
                                                                      theorem CauSeq.lt_total {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (f g : CauSeq α abs) :
                                                                      f < g f g g < f
                                                                      theorem CauSeq.le_total {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (f g : CauSeq α abs) :
                                                                      f g g f
                                                                      theorem CauSeq.const_lt {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {x y : α} :
                                                                      const abs x < const abs y x < y
                                                                      theorem CauSeq.const_le {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {x y : α} :
                                                                      theorem CauSeq.le_of_exists {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {f g : CauSeq α abs} (h : ∃ (i : ), ji, f j g j) :
                                                                      f g
                                                                      theorem CauSeq.exists_gt {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (f : CauSeq α abs) :
                                                                      ∃ (a : α), f < const abs a
                                                                      theorem CauSeq.exists_lt {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (f : CauSeq α abs) :
                                                                      ∃ (a : α), const abs a < f
                                                                      theorem CauSeq.rat_sup_continuous_lemma {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {ε a₁ a₂ b₁ b₂ : α} :
                                                                      |a₁ - b₁| < ε|a₂ - b₂| < ε|max a₁ a₂ - max b₁ b₂| < ε
                                                                      theorem CauSeq.rat_inf_continuous_lemma {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {ε a₁ a₂ b₁ b₂ : α} :
                                                                      |a₁ - b₁| < ε|a₂ - b₂| < ε|min a₁ a₂ - min b₁ b₂| < ε
                                                                      instance CauSeq.instMaxAbs {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] :
                                                                      Equations
                                                                        instance CauSeq.instMinAbs {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] :
                                                                        Equations
                                                                          @[simp]
                                                                          theorem CauSeq.coe_sup {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (f g : CauSeq α abs) :
                                                                          (fg) = fg
                                                                          @[simp]
                                                                          theorem CauSeq.coe_inf {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (f g : CauSeq α abs) :
                                                                          (fg) = fg
                                                                          theorem CauSeq.sup_limZero {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {f g : CauSeq α abs} (hf : f.LimZero) (hg : g.LimZero) :
                                                                          (fg).LimZero
                                                                          theorem CauSeq.inf_limZero {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {f g : CauSeq α abs} (hf : f.LimZero) (hg : g.LimZero) :
                                                                          (fg).LimZero
                                                                          theorem CauSeq.sup_equiv_sup {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a₁ b₁ a₂ b₂ : CauSeq α abs} (ha : a₁ a₂) (hb : b₁ b₂) :
                                                                          a₁b₁ a₂b₂
                                                                          theorem CauSeq.inf_equiv_inf {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a₁ b₁ a₂ b₂ : CauSeq α abs} (ha : a₁ a₂) (hb : b₁ b₂) :
                                                                          a₁b₁ a₂b₂
                                                                          theorem CauSeq.sup_lt {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b c : CauSeq α abs} (ha : a < c) (hb : b < c) :
                                                                          ab < c
                                                                          theorem CauSeq.lt_inf {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b c : CauSeq α abs} (hb : a < b) (hc : a < c) :
                                                                          a < bc
                                                                          @[simp]
                                                                          theorem CauSeq.sup_idem {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (a : CauSeq α abs) :
                                                                          aa = a
                                                                          @[simp]
                                                                          theorem CauSeq.inf_idem {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (a : CauSeq α abs) :
                                                                          aa = a
                                                                          theorem CauSeq.sup_comm {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (a b : CauSeq α abs) :
                                                                          ab = ba
                                                                          theorem CauSeq.inf_comm {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (a b : CauSeq α abs) :
                                                                          ab = ba
                                                                          theorem CauSeq.sup_eq_right {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : CauSeq α abs} (h : a b) :
                                                                          ab b
                                                                          theorem CauSeq.inf_eq_right {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : CauSeq α abs} (h : b a) :
                                                                          ab b
                                                                          theorem CauSeq.sup_eq_left {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : CauSeq α abs} (h : b a) :
                                                                          ab a
                                                                          theorem CauSeq.inf_eq_left {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : CauSeq α abs} (h : a b) :
                                                                          ab a
                                                                          theorem CauSeq.le_sup_left {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : CauSeq α abs} :
                                                                          a ab
                                                                          theorem CauSeq.inf_le_left {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : CauSeq α abs} :
                                                                          ab a
                                                                          theorem CauSeq.le_sup_right {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : CauSeq α abs} :
                                                                          b ab
                                                                          theorem CauSeq.inf_le_right {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : CauSeq α abs} :
                                                                          ab b
                                                                          theorem CauSeq.sup_le {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b c : CauSeq α abs} (ha : a c) (hb : b c) :
                                                                          ab c
                                                                          theorem CauSeq.le_inf {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b c : CauSeq α abs} (hb : a b) (hc : a c) :
                                                                          a bc

                                                                          Note that DistribLattice (CauSeq α abs) is not true because there is no PartialOrder.

                                                                          theorem CauSeq.sup_inf_distrib_left {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (a b c : CauSeq α abs) :
                                                                          abc = (ab)(ac)
                                                                          theorem CauSeq.sup_inf_distrib_right {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (a b c : CauSeq α abs) :
                                                                          abc = (ac)(bc)