Documentation

Mathlib.Data.Real.CauSeq

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 exists_forall_ge_and {α : Type u_1} [LinearOrder α] {P : αProp} {Q : αProp} :
(∃ (i : α), ji, P j)(∃ (i : α), ji, Q j)∃ (i : α), ji, P j Q j
theorem rat_add_continuous_lemma {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [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} [LinearOrderedField α] [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_2} [LinearOrderedField α] {β : Type u_1} [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_1} [LinearOrderedField α] {β : Type u_2} [Ring β] (abv : βα) (f : β) :

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

Equations
  • IsCauSeq abv f = ε > 0, ∃ (i : ), ji, abv (f j - f i) < ε
Instances For
    theorem IsCauSeq.cauchy₂ {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : β} (hf : IsCauSeq abv f) {ε : α} (ε0 : 0 < ε) :
    ∃ (i : ), ji, ki, abv (f j - f k) < ε
    theorem IsCauSeq.cauchy₃ {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : β} (hf : IsCauSeq abv f) {ε : α} (ε0 : 0 < ε) :
    ∃ (i : ), ji, kj, abv (f k - f j) < ε
    theorem IsCauSeq.add {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : β} {g : β} (hf : IsCauSeq abv f) (hg : IsCauSeq abv g) :
    IsCauSeq abv (f + g)
    def CauSeq {α : Type u_1} [LinearOrderedField α] (β : Type u_2) [Ring β] (abv : βα) :
    Type u_2

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

    Equations
    Instances For
      instance CauSeq.instCoeFunCauSeqForAllNat {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [Ring β] {abv : βα} :
      CoeFun (CauSeq β abv) fun (x : CauSeq β abv) => β
      Equations
      • CauSeq.instCoeFunCauSeqForAllNat = { coe := Subtype.val }
      theorem CauSeq.ext {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} {f : CauSeq β abv} {g : CauSeq β abv} (h : ∀ (i : ), f i = g i) :
      f = g
      theorem CauSeq.isCauSeq {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} (f : CauSeq β abv) :
      IsCauSeq abv f
      theorem CauSeq.cauchy {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} (f : CauSeq β abv) {ε : α} :
      0 < ε∃ (i : ), ji, abv (f j - f i) < ε
      def CauSeq.ofEq {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [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
      • CauSeq.ofEq f g e = { val := g, property := (_ : ε > 0, ∃ (i : ), ji, abv (g j - g i) < ε) }
      Instances For
        theorem CauSeq.cauchy₂ {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) {ε : α} :
        0 < ε∃ (i : ), ji, ki, abv (f j - f k) < ε
        theorem CauSeq.cauchy₃ {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) {ε : α} :
        0 < ε∃ (i : ), ji, kj, abv (f k - f j) < ε
        theorem CauSeq.bounded {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) :
        ∃ (r : α), ∀ (i : ), abv (f i) < r
        theorem CauSeq.bounded' {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) (x : α) :
        ∃ r > x, ∀ (i : ), abv (f i) < r
        instance CauSeq.instAddCauSeq {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
        Add (CauSeq β abv)
        Equations
        • CauSeq.instAddCauSeq = { add := fun (f g : CauSeq β abv) => { val := f + g, property := (_ : IsCauSeq abv (f + g)) } }
        @[simp]
        theorem CauSeq.coe_add {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) (g : CauSeq β abv) :
        (f + g) = f + g
        @[simp]
        theorem CauSeq.add_apply {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) (g : CauSeq β abv) (i : ) :
        (f + g) i = f i + g i
        def CauSeq.const {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [Ring β] (abv : βα) [IsAbsoluteValue abv] (x : β) :
        CauSeq β abv

        The constant Cauchy sequence.

        Equations
        • CauSeq.const abv x = { val := fun (x_1 : ) => x, property := (_ : ε > 0, ∃ (i : ), ji, abv ((fun (x_1 : ) => x) j - (fun (x_1 : ) => x) i) < ε) }
        Instances For
          @[simp]
          theorem CauSeq.coe_const {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (x : β) :
          @[simp]
          theorem CauSeq.const_apply {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (x : β) (i : ) :
          (CauSeq.const abv x) i = x
          theorem CauSeq.const_inj {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {x : β} {y : β} :
          CauSeq.const abv x = CauSeq.const abv y x = y
          instance CauSeq.instZeroCauSeq {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
          Zero (CauSeq β abv)
          Equations
          instance CauSeq.instOneCauSeq {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
          One (CauSeq β abv)
          Equations
          instance CauSeq.instInhabitedCauSeq {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
          Inhabited (CauSeq β abv)
          Equations
          • CauSeq.instInhabitedCauSeq = { default := 0 }
          @[simp]
          theorem CauSeq.coe_zero {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
          0 = 0
          @[simp]
          theorem CauSeq.coe_one {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
          1 = 1
          @[simp]
          theorem CauSeq.zero_apply {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (i : ) :
          0 i = 0
          @[simp]
          theorem CauSeq.one_apply {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (i : ) :
          1 i = 1
          @[simp]
          theorem CauSeq.const_zero {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
          CauSeq.const abv 0 = 0
          @[simp]
          theorem CauSeq.const_one {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
          CauSeq.const abv 1 = 1
          theorem CauSeq.const_add {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (x : β) (y : β) :
          CauSeq.const abv (x + y) = CauSeq.const abv x + CauSeq.const abv y
          instance CauSeq.instMulCauSeq {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
          Mul (CauSeq β abv)
          Equations
          • CauSeq.instMulCauSeq = { mul := fun (f g : CauSeq β abv) => { val := f * g, property := (_ : x > 0, ∃ (i : ), ji, abv ((f * g) j - (f * g) i) < x) } }
          @[simp]
          theorem CauSeq.coe_mul {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) (g : CauSeq β abv) :
          (f * g) = f * g
          @[simp]
          theorem CauSeq.mul_apply {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) (g : CauSeq β abv) (i : ) :
          (f * g) i = f i * g i
          theorem CauSeq.const_mul {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (x : β) (y : β) :
          CauSeq.const abv (x * y) = CauSeq.const abv x * CauSeq.const abv y
          instance CauSeq.instNegCauSeq {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
          Neg (CauSeq β abv)
          Equations
          @[simp]
          theorem CauSeq.coe_neg {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) :
          (-f) = -f
          @[simp]
          theorem CauSeq.neg_apply {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) (i : ) :
          (-f) i = -f i
          theorem CauSeq.const_neg {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (x : β) :
          instance CauSeq.instSubCauSeq {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
          Sub (CauSeq β abv)
          Equations
          • CauSeq.instSubCauSeq = { sub := fun (f g : CauSeq β abv) => CauSeq.ofEq (f + -g) (fun (x : ) => f x - g x) (_ : ∀ (i : ), f i + -g i = f i - g i) }
          @[simp]
          theorem CauSeq.coe_sub {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) (g : CauSeq β abv) :
          (f - g) = f - g
          @[simp]
          theorem CauSeq.sub_apply {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) (g : CauSeq β abv) (i : ) :
          (f - g) i = f i - g i
          theorem CauSeq.const_sub {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (x : β) (y : β) :
          CauSeq.const abv (x - y) = CauSeq.const abv x - CauSeq.const abv y
          instance CauSeq.instSMulCauSeq {α : Type u_1} {β : Type u_2} {G : Type u_3} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] [SMul G β] [IsScalarTower G β β] :
          SMul G (CauSeq β abv)
          Equations
          @[simp]
          theorem CauSeq.coe_smul {α : Type u_2} {β : Type u_1} {G : Type u_3} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] [SMul G β] [IsScalarTower G β β] (a : G) (f : CauSeq β abv) :
          (a f) = a f
          @[simp]
          theorem CauSeq.smul_apply {α : Type u_2} {β : Type u_1} {G : Type u_3} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] [SMul G β] [IsScalarTower G β β] (a : G) (f : CauSeq β abv) (i : ) :
          (a f) i = a f i
          theorem CauSeq.const_smul {α : Type u_2} {β : Type u_1} {G : Type u_3} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] [SMul G β] [IsScalarTower G β β] (a : G) (x : β) :
          CauSeq.const abv (a x) = a CauSeq.const abv x
          instance CauSeq.instIsScalarTowerCauSeqInstSMulCauSeqToSMulInstMulCauSeq {α : Type u_1} {β : Type u_2} {G : Type u_3} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] [SMul G β] [IsScalarTower G β β] :
          IsScalarTower G (CauSeq β abv) (CauSeq β abv)
          Equations
          instance CauSeq.addGroup {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
          AddGroup (CauSeq β abv)
          Equations
          • One or more equations did not get rendered due to their size.
          instance CauSeq.instNatCast {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
          NatCast (CauSeq β abv)
          Equations
          instance CauSeq.instIntCast {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
          IntCast (CauSeq β abv)
          Equations
          instance CauSeq.addGroupWithOne {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
          Equations
          • One or more equations did not get rendered due to their size.
          instance CauSeq.instPowCauSeqNat {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
          Pow (CauSeq β abv)
          Equations
          @[simp]
          theorem CauSeq.coe_pow {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) (n : ) :
          (f ^ n) = f ^ n
          @[simp]
          theorem CauSeq.pow_apply {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) (n : ) (i : ) :
          (f ^ n) i = f i ^ n
          theorem CauSeq.const_pow {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (x : β) (n : ) :
          CauSeq.const abv (x ^ n) = CauSeq.const abv x ^ n
          instance CauSeq.ring {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
          Ring (CauSeq β abv)
          Equations
          • One or more equations did not get rendered due to their size.
          instance CauSeq.instCommRingCauSeqToRing {α : Type u_2} [LinearOrderedField α] {β : Type u_1} [CommRing β] {abv : βα} [IsAbsoluteValue abv] :
          CommRing (CauSeq β abv)
          Equations
          • CauSeq.instCommRingCauSeqToRing = let src := CauSeq.ring; CommRing.mk (_ : ∀ (a b : CauSeq β abv), a * b = b * a)
          def CauSeq.LimZero {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [Ring β] {abv : βα} (f : CauSeq β abv) :

          LimZero f holds when f approaches 0.

          Equations
          Instances For
            theorem CauSeq.add_limZero {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : CauSeq β abv} {g : CauSeq β abv} (hf : CauSeq.LimZero f) (hg : CauSeq.LimZero g) :
            theorem CauSeq.mul_limZero_right {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) {g : CauSeq β abv} (hg : CauSeq.LimZero g) :
            theorem CauSeq.mul_limZero_left {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : CauSeq β abv} (g : CauSeq β abv) (hg : CauSeq.LimZero f) :
            theorem CauSeq.neg_limZero {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : CauSeq β abv} (hf : CauSeq.LimZero f) :
            theorem CauSeq.sub_limZero {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : CauSeq β abv} {g : CauSeq β abv} (hf : CauSeq.LimZero f) (hg : CauSeq.LimZero g) :
            theorem CauSeq.limZero_sub_rev {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : CauSeq β abv} {g : CauSeq β abv} (hfg : CauSeq.LimZero (f - g)) :
            theorem CauSeq.zero_limZero {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
            theorem CauSeq.const_limZero {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {x : β} :
            instance CauSeq.equiv {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] :
            Setoid (CauSeq β abv)
            Equations
            theorem CauSeq.add_equiv_add {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f1 : CauSeq β abv} {f2 : CauSeq β abv} {g1 : CauSeq β abv} {g2 : CauSeq β abv} (hf : f1 f2) (hg : g1 g2) :
            f1 + g1 f2 + g2
            theorem CauSeq.neg_equiv_neg {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : CauSeq β abv} {g : CauSeq β abv} (hf : f g) :
            -f -g
            theorem CauSeq.sub_equiv_sub {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f1 : CauSeq β abv} {f2 : CauSeq β abv} {g1 : CauSeq β abv} {g2 : CauSeq β abv} (hf : f1 f2) (hg : g1 g2) :
            f1 - g1 f2 - g2
            theorem CauSeq.equiv_def₃ {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : CauSeq β abv} {g : CauSeq β abv} (h : f g) {ε : α} (ε0 : 0 < ε) :
            ∃ (i : ), ji, kj, abv (f k - g j) < ε
            theorem CauSeq.limZero_congr {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : CauSeq β abv} {g : CauSeq β abv} (h : f g) :
            theorem CauSeq.abv_pos_of_not_limZero {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : CauSeq β abv} (hf : ¬CauSeq.LimZero f) :
            ∃ K > 0, ∃ (i : ), ji, K abv (f j)
            theorem CauSeq.of_near {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [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_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : CauSeq β abv} (hf : ¬f 0) :
            theorem CauSeq.mul_equiv_zero {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (g : CauSeq β abv) {f : CauSeq β abv} (hf : f 0) :
            g * f 0
            theorem CauSeq.mul_equiv_zero' {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] (g : CauSeq β abv) {f : CauSeq β abv} (hf : f 0) :
            f * g 0
            theorem CauSeq.mul_not_equiv_zero {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : CauSeq β abv} {g : CauSeq β abv} (hf : ¬f 0) (hg : ¬g 0) :
            ¬f * g 0
            theorem CauSeq.const_equiv {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {x : β} {y : β} :
            theorem CauSeq.mul_equiv_mul {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f1 : CauSeq β abv} {f2 : CauSeq β abv} {g1 : CauSeq β abv} {g2 : CauSeq β abv} (hf : f1 f2) (hg : g1 g2) :
            f1 * g1 f2 * g2
            theorem CauSeq.smul_equiv_smul {α : Type u_3} {β : Type u_2} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {G : Type u_1} [SMul G β] [IsScalarTower G β β] {f1 : CauSeq β abv} {f2 : CauSeq β abv} (c : G) (hf : f1 f2) :
            c f1 c f2
            theorem CauSeq.pow_equiv_pow {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f1 : CauSeq β abv} {f2 : CauSeq β abv} (hf : f1 f2) (n : ) :
            f1 ^ n f2 ^ n
            theorem CauSeq.one_not_equiv_zero {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [Ring β] [IsDomain β] (abv : βα) [IsAbsoluteValue abv] :
            theorem CauSeq.inv_aux {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] {f : CauSeq β abv} (hf : ¬CauSeq.LimZero f) (ε : α) :
            ε > 0∃ (i : ), ji, abv ((f j)⁻¹ - (f i)⁻¹) < ε
            def CauSeq.inv {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) (hf : ¬CauSeq.LimZero f) :
            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_2} {β : Type u_1} [LinearOrderedField α] [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] {f : CauSeq β abv} (hf : ¬CauSeq.LimZero f) :
              (CauSeq.inv f hf) = (f)⁻¹
              @[simp]
              theorem CauSeq.inv_apply {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] {f : CauSeq β abv} (hf : ¬CauSeq.LimZero f) (i : ) :
              (CauSeq.inv f hf) i = (f i)⁻¹
              theorem CauSeq.inv_mul_cancel {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] {f : CauSeq β abv} (hf : ¬CauSeq.LimZero f) :
              CauSeq.inv f hf * f 1
              theorem CauSeq.mul_inv_cancel {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] {f : CauSeq β abv} (hf : ¬CauSeq.LimZero f) :
              f * CauSeq.inv f hf 1
              theorem CauSeq.const_inv {α : Type u_2} {β : Type u_1} [LinearOrderedField α] [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] {x : β} (hx : x 0) :
              def CauSeq.Pos {α : Type u_1} [LinearOrderedField α] (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} [LinearOrderedField α] {x : α} :
                theorem CauSeq.add_pos {α : Type u_1} [LinearOrderedField α] {f : CauSeq α abs} {g : CauSeq α abs} :
                CauSeq.Pos fCauSeq.Pos gCauSeq.Pos (f + g)
                theorem CauSeq.pos_add_limZero {α : Type u_1} [LinearOrderedField α] {f : CauSeq α abs} {g : CauSeq α abs} :
                theorem CauSeq.mul_pos {α : Type u_1} [LinearOrderedField α] {f : CauSeq α abs} {g : CauSeq α abs} :
                CauSeq.Pos fCauSeq.Pos gCauSeq.Pos (f * g)
                theorem CauSeq.lt_of_lt_of_eq {α : Type u_1} [LinearOrderedField α] {f : CauSeq α abs} {g : CauSeq α abs} {h : CauSeq α abs} (fg : f < g) (gh : g h) :
                f < h
                theorem CauSeq.lt_of_eq_of_lt {α : Type u_1} [LinearOrderedField α] {f : CauSeq α abs} {g : CauSeq α abs} {h : CauSeq α abs} (fg : f g) (gh : g < h) :
                f < h
                theorem CauSeq.lt_trans {α : Type u_1} [LinearOrderedField α] {f : CauSeq α abs} {g : CauSeq α abs} {h : CauSeq α abs} (fg : f < g) (gh : g < h) :
                f < h
                theorem CauSeq.lt_irrefl {α : Type u_1} [LinearOrderedField α] {f : CauSeq α abs} :
                ¬f < f
                theorem CauSeq.le_of_eq_of_le {α : Type u_1} [LinearOrderedField α] {f : CauSeq α abs} {g : CauSeq α abs} {h : CauSeq α abs} (hfg : f g) (hgh : g h) :
                f h
                theorem CauSeq.le_of_le_of_eq {α : Type u_1} [LinearOrderedField α] {f : CauSeq α abs} {g : CauSeq α abs} {h : CauSeq α abs} (hfg : f g) (hgh : g h) :
                f h
                theorem CauSeq.le_antisymm {α : Type u_1} [LinearOrderedField α] {f : CauSeq α abs} {g : CauSeq α abs} (fg : f g) (gf : g f) :
                f g
                theorem CauSeq.lt_total {α : Type u_1} [LinearOrderedField α] (f : CauSeq α abs) (g : CauSeq α abs) :
                f < g f g g < f
                theorem CauSeq.le_total {α : Type u_1} [LinearOrderedField α] (f : CauSeq α abs) (g : CauSeq α abs) :
                f g g f
                theorem CauSeq.const_lt {α : Type u_1} [LinearOrderedField α] {x : α} {y : α} :
                CauSeq.const abs x < CauSeq.const abs y x < y
                theorem CauSeq.const_le {α : Type u_1} [LinearOrderedField α] {x : α} {y : α} :
                theorem CauSeq.le_of_exists {α : Type u_1} [LinearOrderedField α] {f : CauSeq α abs} {g : CauSeq α abs} (h : ∃ (i : ), ji, f j g j) :
                f g
                theorem CauSeq.exists_gt {α : Type u_1} [LinearOrderedField α] (f : CauSeq α abs) :
                ∃ (a : α), f < CauSeq.const abs a
                theorem CauSeq.exists_lt {α : Type u_1} [LinearOrderedField α] (f : CauSeq α abs) :
                ∃ (a : α), CauSeq.const abs a < f
                theorem CauSeq.rat_sup_continuous_lemma {α : Type u_1} [LinearOrderedField α] {ε : α} {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
                |a₁ - b₁| < ε|a₂ - b₂| < ε|a₁ a₂ - b₁ b₂| < ε
                theorem CauSeq.rat_inf_continuous_lemma {α : Type u_1} [LinearOrderedField α] {ε : α} {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
                |a₁ - b₁| < ε|a₂ - b₂| < ε|a₁ a₂ - b₁ b₂| < ε
                @[simp]
                theorem CauSeq.coe_sup {α : Type u_1} [LinearOrderedField α] (f : CauSeq α abs) (g : CauSeq α abs) :
                (f g) = f g
                @[simp]
                theorem CauSeq.coe_inf {α : Type u_1} [LinearOrderedField α] (f : CauSeq α abs) (g : CauSeq α abs) :
                (f g) = f g
                theorem CauSeq.sup_limZero {α : Type u_1} [LinearOrderedField α] {f : CauSeq α abs} {g : CauSeq α abs} (hf : CauSeq.LimZero f) (hg : CauSeq.LimZero g) :
                theorem CauSeq.inf_limZero {α : Type u_1} [LinearOrderedField α] {f : CauSeq α abs} {g : CauSeq α abs} (hf : CauSeq.LimZero f) (hg : CauSeq.LimZero g) :
                theorem CauSeq.sup_equiv_sup {α : Type u_1} [LinearOrderedField α] {a₁ : CauSeq α abs} {b₁ : CauSeq α abs} {a₂ : CauSeq α abs} {b₂ : CauSeq α abs} (ha : a₁ a₂) (hb : b₁ b₂) :
                a₁ b₁ a₂ b₂
                theorem CauSeq.inf_equiv_inf {α : Type u_1} [LinearOrderedField α] {a₁ : CauSeq α abs} {b₁ : CauSeq α abs} {a₂ : CauSeq α abs} {b₂ : CauSeq α abs} (ha : a₁ a₂) (hb : b₁ b₂) :
                a₁ b₁ a₂ b₂
                theorem CauSeq.sup_lt {α : Type u_1} [LinearOrderedField α] {a : CauSeq α abs} {b : CauSeq α abs} {c : CauSeq α abs} (ha : a < c) (hb : b < c) :
                a b < c
                theorem CauSeq.lt_inf {α : Type u_1} [LinearOrderedField α] {a : CauSeq α abs} {b : CauSeq α abs} {c : CauSeq α abs} (hb : a < b) (hc : a < c) :
                a < b c
                @[simp]
                theorem CauSeq.sup_idem {α : Type u_1} [LinearOrderedField α] (a : CauSeq α abs) :
                a a = a
                @[simp]
                theorem CauSeq.inf_idem {α : Type u_1} [LinearOrderedField α] (a : CauSeq α abs) :
                a a = a
                theorem CauSeq.sup_comm {α : Type u_1} [LinearOrderedField α] (a : CauSeq α abs) (b : CauSeq α abs) :
                a b = b a
                theorem CauSeq.inf_comm {α : Type u_1} [LinearOrderedField α] (a : CauSeq α abs) (b : CauSeq α abs) :
                a b = b a
                theorem CauSeq.sup_eq_right {α : Type u_1} [LinearOrderedField α] {a : CauSeq α abs} {b : CauSeq α abs} (h : a b) :
                a b b
                theorem CauSeq.inf_eq_right {α : Type u_1} [LinearOrderedField α] {a : CauSeq α abs} {b : CauSeq α abs} (h : b a) :
                a b b
                theorem CauSeq.sup_eq_left {α : Type u_1} [LinearOrderedField α] {a : CauSeq α abs} {b : CauSeq α abs} (h : b a) :
                a b a
                theorem CauSeq.inf_eq_left {α : Type u_1} [LinearOrderedField α] {a : CauSeq α abs} {b : CauSeq α abs} (h : a b) :
                a b a
                theorem CauSeq.le_sup_left {α : Type u_1} [LinearOrderedField α] {a : CauSeq α abs} {b : CauSeq α abs} :
                a a b
                theorem CauSeq.inf_le_left {α : Type u_1} [LinearOrderedField α] {a : CauSeq α abs} {b : CauSeq α abs} :
                a b a
                theorem CauSeq.le_sup_right {α : Type u_1} [LinearOrderedField α] {a : CauSeq α abs} {b : CauSeq α abs} :
                b a b
                theorem CauSeq.inf_le_right {α : Type u_1} [LinearOrderedField α] {a : CauSeq α abs} {b : CauSeq α abs} :
                a b b
                theorem CauSeq.sup_le {α : Type u_1} [LinearOrderedField α] {a : CauSeq α abs} {b : CauSeq α abs} {c : CauSeq α abs} (ha : a c) (hb : b c) :
                a b c
                theorem CauSeq.le_inf {α : Type u_1} [LinearOrderedField α] {a : CauSeq α abs} {b : CauSeq α abs} {c : CauSeq α abs} (hb : a b) (hc : a c) :
                a b c

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

                theorem CauSeq.sup_inf_distrib_left {α : Type u_1} [LinearOrderedField α] (a : CauSeq α abs) (b : CauSeq α abs) (c : CauSeq α abs) :
                a b c = (a b) (a c)
                theorem CauSeq.sup_inf_distrib_right {α : Type u_1} [LinearOrderedField α] (a : CauSeq α abs) (b : CauSeq α abs) (c : CauSeq α abs) :
                a b c = (a c) (b c)