Analysis
6.1. Convergence and limit laws

Imports

import Mathlib.Tactic
import Analysis.Section_5_1
import Analysis.Section_5_3
import Analysis.Section_5_epilogue

Analysis I, Section 6.1: Convergence and limit laws

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

Definition of ε-closeness, ε-steadiness, and their eventual counterparts.
Notion of a Cauchy sequence, convergent sequence, and bounded sequence of reals.

/- Definition 6.1.1 (Distance).  Here we use the Mathlib distance. -/
Real.dist_eq (x y : ℝ) : dist x y = |x - y|#check Real.dist_eq

abbrev Real.Close (ε x y : ℝ) : Prop := dist x y ≤ ε

Definition 6.1.2 (ε-close). This is similar to the previous notion of ε-closeness, but where all quantities are real instead of rational.

theorem Real.close_def (ε x y : ℝ) : ε.Close x y ↔ dist x y ≤ ε := byε:ℝx:ℝy:ℝ⊢ ε.Close x y ↔ dist x y ≤ ε rflAll goals completed! 🐙

namespace Chapter6

Definition 6.1.3 (Sequence). This is similar to the Chapter 5 sequence, except that now the sequence is real-valued. As with Chapter 5, we start sequences from 0 by default.

@[ext]
structure Sequence where
  m : ℤ
  seq : ℤ → ℝ
  vanish : ∀ n < m, seq n = 0

Sequences can be thought of as functions from ℤ to ℝ.

instance Sequence.instCoeFun : CoeFun Sequence (fun _ ↦ ℤ → ℝ) where
  coe a := a.seq

@[coe]
abbrev Sequence.ofNatFun (a:ℕ → ℝ) : Sequence :=
 {
    m := 0
    seq n := if n ≥ 0 then a n.toNat else 0
    vanish := bya:ℕ → ℝ⊢ ∀ n < 0, (if n ≥ 0 then a n.toNat else 0) = 0 simp_allAll goals completed! 🐙
 }

Functions from ℕ to ℝ can be thought of as sequences.

instance Sequence.instCoe : Coe (ℕ → ℝ) Sequence where
  coe := ofNatFun

              abbrev Sequence.mk' (m:ℤ) (a: { n // n ≥ m } → ℝ) : Sequence where
  m := m
  seq n := if h : n ≥ m then a ⟨n, h⟩ else 0
  vanish := bym:ℤa:{ n // n ≥ m } → ℝ⊢ ∀ n < m, (if h : n ≥ m then a ⟨n, h⟩ else 0) = 0 simp_allAll goals completed! 🐙lemma Sequence.eval_mk {n m:ℤ} (a: { n // n ≥ m } → ℝ) (h: n ≥ m) :
    (Sequence.mk' m a) n = a ⟨ n, h ⟩ := byn:ℤm:ℤa:{ n // n ≥ m } → ℝh:n ≥ m⊢ (mk' m a).seq n = a ⟨n, h⟩ simp [h]All goals completed! 🐙@[simp]
lemma Sequence.eval_coe (n:ℕ) (a: ℕ → ℝ) : (a:Sequence) n = a n := byn:ℕa:ℕ → ℝ⊢ (↑a).seq ↑n = a n simpAll goals completed! 🐙

a.from n₁ starts a : Sequence from n₁. It is intended for use when n₁ ≥ n₀, but returns the "junk" value of the original sequence a otherwise.

abbrev Sequence.from (a:Sequence) (m₁:ℤ) : Sequence := mk' (max a.m m₁) (a ↑·)

lemma Sequence.from_eval (a:Sequence) {m₁ n:ℤ} (hn: n ≥ m₁) :
  (a.from m₁) n = a n := bya:Sequencem₁:ℤn:ℤhn:n ≥ m₁⊢ (a.from m₁).seq n = a.seq n
  simp [hn]a:Sequencem₁:ℤn:ℤhn:n ≥ m₁⊢ n < a.m → 0 = a.seq n; introsa:Sequencem₁:ℤn:ℤhn:n ≥ m₁a✝:n < a.m⊢ 0 = a.seq n; symma:Sequencem₁:ℤn:ℤhn:n ≥ m₁a✝:n < a.m⊢ a.seq n = 0; solve_by_elim [a.vanish]All goals completed! 🐙

end Chapter6

Definition 6.1.3 (ε-steady)

abbrev Real.Steady (ε: ℝ) (a: Chapter6.Sequence) : Prop :=
  ∀ n ≥ a.m, ∀ m ≥ a.m, ε.Close (a n) (a m)

Definition 6.1.3 (ε-steady, def)

lemma Real.steady_def (ε: ℝ) (a: Chapter6.Sequence) :
  ε.Steady a ↔ ∀ n ≥ a.m, ∀ m ≥ a.m, ε.Close (a n) (a m) := byε:ℝa:Chapter6.Sequence⊢ ε.Steady a ↔ ∀ n ≥ a.m, ∀ m ≥ a.m, ε.Close (a.seq n) (a.seq m) rflAll goals completed! 🐙

Definition 6.1.3 (Eventually ε-steady)

abbrev Real.EventuallySteady (ε: ℝ) (a: Chapter6.Sequence) : Prop :=
  ∃ N ≥ a.m, ε.Steady (a.from N)

Definition 6.1.3 (Eventually ε-steady, def)

lemma Real.eventuallySteady_def (ε: ℝ) (a: Chapter6.Sequence) :
  ε.EventuallySteady a ↔ ∃ N, (N ≥ a.m) ∧ ε.Steady (a.from N) := byε:ℝa:Chapter6.Sequence⊢ ε.EventuallySteady a ↔ ∃ N ≥ a.m, ε.Steady (a.from N) rflAll goals completed! 🐙

For fixed a, the function ε ↦ ε.Steady s is monotone

theorem Real.Steady.mono {a: Chapter6.Sequence} {ε₁ ε₂: ℝ} (hε: ε₁ ≤ ε₂) (hsteady: ε₁.Steady a) :
    ε₂.Steady a := bya:Chapter6.Sequenceε₁:ℝε₂:ℝhε:ε₁ ≤ ε₂hsteady:ε₁.Steady a⊢ ε₂.Steady a grindAll goals completed! 🐙

For fixed a, the function ε ↦ ε.EventuallySteady s is monotone

theorem Real.EventuallySteady.mono {a: Chapter6.Sequence} {ε₁ ε₂: ℝ} (hε: ε₁ ≤ ε₂)
  (hsteady: ε₁.EventuallySteady a) :
    ε₂.EventuallySteady a := bya:Chapter6.Sequenceε₁:ℝε₂:ℝhε:ε₁ ≤ ε₂hsteady:ε₁.EventuallySteady a⊢ ε₂.EventuallySteady a peel 2 hsteadyh.ha:Chapter6.Sequenceε₁:ℝε₂:ℝhε:ε₁ ≤ ε₂hsteady:ε₁.EventuallySteady aN✝:ℤp✝:N✝ ≥ a.mthis:ε₁.Steady (a.from N✝)⊢ ε₂.Steady (a.from N✝); grind [Steady.mono]All goals completed! 🐙

namespace Chapter6

Definition 6.1.3 (Cauchy sequence)

abbrev Sequence.IsCauchy (a:Sequence) : Prop := ∀ ε > (0:ℝ), ε.EventuallySteady a

Definition 6.1.3 (Cauchy sequence, def)

lemma Sequence.isCauchy_def (a:Sequence) :
  a.IsCauchy ↔ ∀ ε > (0:ℝ), ε.EventuallySteady a := bya:Sequence⊢ a.IsCauchy ↔ ∀ ε > 0, ε.EventuallySteady a rflAll goals completed! 🐙

This is almost the same as Chapter5.Sequence.IsCauchy.coe

lemma Sequence.IsCauchy.coe (a:ℕ → ℝ) :
    (a:Sequence).IsCauchy ↔ ∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, dist (a j) (a k) ≤ ε := bya:ℕ → ℝ⊢ (↑a).IsCauchy ↔ ∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, dist (a j) (a k) ≤ ε
  peel with ε hεh.ha:ℕ → ℝε:ℝhε:ε > 0⊢ ε.EventuallySteady ↑a ↔ ∃ N, ∀ j ≥ N, ∀ k ≥ N, dist (a j) (a k) ≤ ε
  constructorh.h.mpa:ℕ → ℝε:ℝhε:ε > 0⊢ ε.EventuallySteady ↑a → ∃ N, ∀ j ≥ N, ∀ k ≥ N, dist (a j) (a k) ≤ εh.h.mpra:ℕ → ℝε:ℝhε:ε > 0⊢ (∃ N, ∀ j ≥ N, ∀ k ≥ N, dist (a j) (a k) ≤ ε) → ε.EventuallySteady ↑a
  ·h.h.mpa:ℕ → ℝε:ℝhε:ε > 0⊢ ε.EventuallySteady ↑a → ∃ N, ∀ j ≥ N, ∀ k ≥ N, dist (a j) (a k) ≤ ε rintro ⟨ N, hN, h' ⟩h.h.mpa:ℕ → ℝε:ℝhε:ε > 0N:ℤhN:N ≥ (↑a).mh':ε.Steady ((↑a).from N)⊢ ∃ N, ∀ j ≥ N, ∀ k ≥ N, dist (a j) (a k) ≤ ε
    lift N to ℕ using hNh.h.mpa:ℕ → ℝε:ℝhε:ε > 0N:ℕh':ε.Steady ((↑a).from ↑N)⊢ ∃ N, ∀ j ≥ N, ∀ k ≥ N, dist (a j) (a k) ≤ ε; use Nha:ℕ → ℝε:ℝhε:ε > 0N:ℕh':ε.Steady ((↑a).from ↑N)⊢ ∀ j ≥ N, ∀ k ≥ N, dist (a j) (a k) ≤ ε
    intro j hjha:ℕ → ℝε:ℝhε:ε > 0N:ℕh':ε.Steady ((↑a).from ↑N)j:ℕhj:j ≥ N⊢ ∀ k ≥ N, dist (a j) (a k) ≤ ε kha:ℕ → ℝε:ℝhε:ε > 0N:ℕh':ε.Steady ((↑a).from ↑N)j:ℕhj:j ≥ Nk:ℕ⊢ k ≥ N → dist (a j) (a k) ≤ ε hkha:ℕ → ℝε:ℝhε:ε > 0N:ℕh':ε.Steady ((↑a).from ↑N)j:ℕhj:j ≥ Nk:ℕhk:k ≥ N⊢ dist (a j) (a k) ≤ ε
    simp [Real.steady_def] at h'ha:ℕ → ℝε:ℝhε:ε > 0N:ℕj:ℕhj:j ≥ Nk:ℕhk:k ≥ Nh':∀ (n : ℤ),
  ↑N ≤ n →
    ∀ (m : ℤ),
      ↑N ≤ m →
        dist (if ↑N ≤ n then if 0 ≤ n then a n.toNat else 0 else 0)
            (if ↑N ≤ m then if 0 ≤ m then a m.toNat else 0 else 0) ≤
          ε⊢ dist (a j) (a k) ≤ ε
    specialize h' j ?_ k ?_h.specialize_1a:ℕ → ℝε:ℝhε:ε > 0N:ℕj:ℕhj:j ≥ Nk:ℕhk:k ≥ Nh':∀ (n : ℤ),
  ↑N ≤ n →
    ∀ (m : ℤ),
      ↑N ≤ m →
        dist (if ↑N ≤ n then if 0 ≤ n then a n.toNat else 0 else 0)
            (if ↑N ≤ m then if 0 ≤ m then a m.toNat else 0 else 0) ≤
          ε⊢ ↑N ≤ ↑jh.specialize_2a:ℕ → ℝε:ℝhε:ε > 0N:ℕj:ℕhj:j ≥ Nk:ℕhk:k ≥ Nh':∀ (n : ℤ),
  ↑N ≤ n →
    ∀ (m : ℤ),
      ↑N ≤ m →
        dist (if ↑N ≤ n then if 0 ≤ n then a n.toNat else 0 else 0)
            (if ↑N ≤ m then if 0 ≤ m then a m.toNat else 0 else 0) ≤
          ε⊢ ↑N ≤ ↑kha:ℕ → ℝε:ℝhε:ε > 0N:ℕj:ℕhj:j ≥ Nk:ℕhk:k ≥ Nh':dist (if ↑N ≤ ↑j then if 0 ≤ ↑j then a (↑j).toNat else 0 else 0)
    (if ↑N ≤ ↑k then if 0 ≤ ↑k then a (↑k).toNat else 0 else 0) ≤
  ε⊢ dist (a j) (a k) ≤ ε <;>h.specialize_1a:ℕ → ℝε:ℝhε:ε > 0N:ℕj:ℕhj:j ≥ Nk:ℕhk:k ≥ Nh':∀ (n : ℤ),
  ↑N ≤ n →
    ∀ (m : ℤ),
      ↑N ≤ m →
        dist (if ↑N ≤ n then if 0 ≤ n then a n.toNat else 0 else 0)
            (if ↑N ≤ m then if 0 ≤ m then a m.toNat else 0 else 0) ≤
          ε⊢ ↑N ≤ ↑jh.specialize_2a:ℕ → ℝε:ℝhε:ε > 0N:ℕj:ℕhj:j ≥ Nk:ℕhk:k ≥ Nh':∀ (n : ℤ),
  ↑N ≤ n →
    ∀ (m : ℤ),
      ↑N ≤ m →
        dist (if ↑N ≤ n then if 0 ≤ n then a n.toNat else 0 else 0)
            (if ↑N ≤ m then if 0 ≤ m then a m.toNat else 0 else 0) ≤
          ε⊢ ↑N ≤ ↑kha:ℕ → ℝε:ℝhε:ε > 0N:ℕj:ℕhj:j ≥ Nk:ℕhk:k ≥ Nh':dist (if ↑N ≤ ↑j then if 0 ≤ ↑j then a (↑j).toNat else 0 else 0)
    (if ↑N ≤ ↑k then if 0 ≤ ↑k then a (↑k).toNat else 0 else 0) ≤
  ε⊢ dist (a j) (a k) ≤ ε try omegaAll goals completed! 🐙
    simp_allAll goals completed! 🐙
  rintro ⟨ N, h' ⟩h.h.mpra:ℕ → ℝε:ℝhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, dist (a j) (a k) ≤ ε⊢ ε.EventuallySteady ↑a; refine ⟨ max N 0, bya:ℕ → ℝε:ℝhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, dist (a j) (a k) ≤ ε⊢ max (↑N) 0 ≥ (↑a).m simpAll goals completed! 🐙, ?_ ⟩
  intro n hnh.h.mpra:ℕ → ℝε:ℝhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, dist (a j) (a k) ≤ εn:ℤhn:n ≥ ((↑a).from (max (↑N) 0)).m⊢ ∀ m ≥ ((↑a).from (max (↑N) 0)).m, ε.Close (((↑a).from (max (↑N) 0)).seq n) (((↑a).from (max (↑N) 0)).seq m) mh.h.mpra:ℕ → ℝε:ℝhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, dist (a j) (a k) ≤ εn:ℤhn:n ≥ ((↑a).from (max (↑N) 0)).mm:ℤ⊢ m ≥ ((↑a).from (max (↑N) 0)).m → ε.Close (((↑a).from (max (↑N) 0)).seq n) (((↑a).from (max (↑N) 0)).seq m) hmh.h.mpra:ℕ → ℝε:ℝhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, dist (a j) (a k) ≤ εn:ℤhn:n ≥ ((↑a).from (max (↑N) 0)).mm:ℤhm:m ≥ ((↑a).from (max (↑N) 0)).m⊢ ε.Close (((↑a).from (max (↑N) 0)).seq n) (((↑a).from (max (↑N) 0)).seq m); simp at hn hmh.h.mpra:ℕ → ℝε:ℝhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ m⊢ ε.Close (((↑a).from (max (↑N) 0)).seq n) (((↑a).from (max (↑N) 0)).seq m)
  have npos : 0 ≤ n := bya:ℕ → ℝ⊢ (↑a).IsCauchy ↔ ∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, dist (a j) (a k) ≤ ε omegaAll goals completed! 🐙
  have mpos : 0 ≤ m := bya:ℕ → ℝ⊢ (↑a).IsCauchy ↔ ∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, dist (a j) (a k) ≤ ε omegaAll goals completed! 🐙
  simp [hn, hm, npos, mpos]h.h.mpra:ℕ → ℝε:ℝhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ mnpos:0 ≤ nmpos:0 ≤ m⊢ dist (a n.toNat) (a m.toNat) ≤ ε
  lift n to ℕ using nposh.h.mpra:ℕ → ℝε:ℝhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, dist (a j) (a k) ≤ εm:ℤhm:↑N ≤ mmpos:0 ≤ mn:ℕhn:↑N ≤ ↑n⊢ dist (a (↑n).toNat) (a m.toNat) ≤ ε
  lift m to ℕ using mposh.h.mpra:ℕ → ℝε:ℝhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, dist (a j) (a k) ≤ εn:ℕhn:↑N ≤ ↑nm:ℕhm:↑N ≤ ↑m⊢ dist (a (↑n).toNat) (a (↑m).toNat) ≤ ε
  specialize h' n ?_ m ?_h.h.mpr.specialize_1a:ℕ → ℝε:ℝhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, dist (a j) (a k) ≤ εn:ℕhn:↑N ≤ ↑nm:ℕhm:↑N ≤ ↑m⊢ n ≥ Nh.h.mpr.specialize_2a:ℕ → ℝε:ℝhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, dist (a j) (a k) ≤ εn:ℕhn:↑N ≤ ↑nm:ℕhm:↑N ≤ ↑m⊢ m ≥ Nh.h.mpra:ℕ → ℝε:ℝhε:ε > 0N:ℕn:ℕhn:↑N ≤ ↑nm:ℕhm:↑N ≤ ↑mh':dist (a n) (a m) ≤ ε⊢ dist (a (↑n).toNat) (a (↑m).toNat) ≤ ε <;>h.h.mpr.specialize_1a:ℕ → ℝε:ℝhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, dist (a j) (a k) ≤ εn:ℕhn:↑N ≤ ↑nm:ℕhm:↑N ≤ ↑m⊢ n ≥ Nh.h.mpr.specialize_2a:ℕ → ℝε:ℝhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, dist (a j) (a k) ≤ εn:ℕhn:↑N ≤ ↑nm:ℕhm:↑N ≤ ↑m⊢ m ≥ Nh.h.mpra:ℕ → ℝε:ℝhε:ε > 0N:ℕn:ℕhn:↑N ≤ ↑nm:ℕhm:↑N ≤ ↑mh':dist (a n) (a m) ≤ ε⊢ dist (a (↑n).toNat) (a (↑m).toNat) ≤ ε try grindAll goals completed! 🐙

              lemma Sequence.IsCauchy.mk {n₀:ℤ} (a: {n // n ≥ n₀} → ℝ) :
    (mk' n₀ a).IsCauchy
    ↔ ∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, dist (mk' n₀ a j) (mk' n₀ a k) ≤ ε := byn₀:ℤa:{ n // n ≥ n₀ } → ℝ⊢ (mk' n₀ a).IsCauchy ↔ ∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε
  peel with ε hεh.hn₀:ℤa:{ n // n ≥ n₀ } → ℝε:ℝhε:ε > 0⊢ ε.EventuallySteady (mk' n₀ a) ↔ ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε
  constructorh.h.mpn₀:ℤa:{ n // n ≥ n₀ } → ℝε:ℝhε:ε > 0⊢ ε.EventuallySteady (mk' n₀ a) → ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ εh.h.mprn₀:ℤa:{ n // n ≥ n₀ } → ℝε:ℝhε:ε > 0⊢ (∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε) → ε.EventuallySteady (mk' n₀ a)
  ·h.h.mpn₀:ℤa:{ n // n ≥ n₀ } → ℝε:ℝhε:ε > 0⊢ ε.EventuallySteady (mk' n₀ a) → ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε rintro ⟨ N, hN, h' ⟩h.h.mpn₀:ℤa:{ n // n ≥ n₀ } → ℝε:ℝhε:ε > 0N:ℤhN:N ≥ (mk' n₀ a).mh':ε.Steady ((mk' n₀ a).from N)⊢ ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε; refine ⟨ N, hN, ?_ ⟩h.h.mpn₀:ℤa:{ n // n ≥ n₀ } → ℝε:ℝhε:ε > 0N:ℤhN:N ≥ (mk' n₀ a).mh':ε.Steady ((mk' n₀ a).from N)⊢ ∀ j ≥ N, ∀ k ≥ N, dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε
    dsimp at hNh.h.mpn₀:ℤa:{ n // n ≥ n₀ } → ℝε:ℝhε:ε > 0N:ℤhN:N ≥ n₀h':ε.Steady ((mk' n₀ a).from N)⊢ ∀ j ≥ N, ∀ k ≥ N, dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε
    intro j hjh.h.mpn₀:ℤa:{ n // n ≥ n₀ } → ℝε:ℝhε:ε > 0N:ℤhN:N ≥ n₀h':ε.Steady ((mk' n₀ a).from N)j:ℤhj:j ≥ N⊢ ∀ k ≥ N, dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε kh.h.mpn₀:ℤa:{ n // n ≥ n₀ } → ℝε:ℝhε:ε > 0N:ℤhN:N ≥ n₀h':ε.Steady ((mk' n₀ a).from N)j:ℤhj:j ≥ Nk:ℤ⊢ k ≥ N → dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε hkh.h.mpn₀:ℤa:{ n // n ≥ n₀ } → ℝε:ℝhε:ε > 0N:ℤhN:N ≥ n₀h':ε.Steady ((mk' n₀ a).from N)j:ℤhj:j ≥ Nk:ℤhk:k ≥ N⊢ dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε
    simp only [Real.Steady, show max n₀ N = N by omega] at h'h.h.mpn₀:ℤa:{ n // n ≥ n₀ } → ℝε:ℝhε:ε > 0N:ℤhN:N ≥ n₀j:ℤhj:j ≥ Nk:ℤhk:k ≥ Nh':∀ n ≥ N,
  ∀ m ≥ N,
    ε.Close (if h : n ≥ N then if h_1 : n ≥ n₀ then a ⟨n, ⋯⟩ else 0 else 0)
      (if h : m ≥ N then if h_1 : m ≥ n₀ then a ⟨m, ⋯⟩ else 0 else 0)⊢ dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε
    specialize h' j ?_ k ?_h.h.mp.specialize_1n₀:ℤa:{ n // n ≥ n₀ } → ℝε:ℝhε:ε > 0N:ℤhN:N ≥ n₀j:ℤhj:j ≥ Nk:ℤhk:k ≥ Nh':∀ n ≥ N,
  ∀ m ≥ N,
    ε.Close (if h : n ≥ N then if h_1 : n ≥ n₀ then a ⟨n, ⋯⟩ else 0 else 0)
      (if h : m ≥ N then if h_1 : m ≥ n₀ then a ⟨m, ⋯⟩ else 0 else 0)⊢ j ≥ Nh.h.mp.specialize_2n₀:ℤa:{ n // n ≥ n₀ } → ℝε:ℝhε:ε > 0N:ℤhN:N ≥ n₀j:ℤhj:j ≥ Nk:ℤhk:k ≥ Nh':∀ n ≥ N,
  ∀ m ≥ N,
    ε.Close (if h : n ≥ N then if h_1 : n ≥ n₀ then a ⟨n, ⋯⟩ else 0 else 0)
      (if h : m ≥ N then if h_1 : m ≥ n₀ then a ⟨m, ⋯⟩ else 0 else 0)⊢ k ≥ Nh.h.mpn₀:ℤa:{ n // n ≥ n₀ } → ℝε:ℝhε:ε > 0N:ℤhN:N ≥ n₀j:ℤhj:j ≥ Nk:ℤhk:k ≥ Nh':ε.Close (if h : j ≥ N then if h_1 : j ≥ n₀ then a ⟨j, ⋯⟩ else 0 else 0)
  (if h : k ≥ N then if h_1 : k ≥ n₀ then a ⟨k, ⋯⟩ else 0 else 0)⊢ dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε <;>h.h.mp.specialize_1n₀:ℤa:{ n // n ≥ n₀ } → ℝε:ℝhε:ε > 0N:ℤhN:N ≥ n₀j:ℤhj:j ≥ Nk:ℤhk:k ≥ Nh':∀ n ≥ N,
  ∀ m ≥ N,
    ε.Close (if h : n ≥ N then if h_1 : n ≥ n₀ then a ⟨n, ⋯⟩ else 0 else 0)
      (if h : m ≥ N then if h_1 : m ≥ n₀ then a ⟨m, ⋯⟩ else 0 else 0)⊢ j ≥ Nh.h.mp.specialize_2n₀:ℤa:{ n // n ≥ n₀ } → ℝε:ℝhε:ε > 0N:ℤhN:N ≥ n₀j:ℤhj:j ≥ Nk:ℤhk:k ≥ Nh':∀ n ≥ N,
  ∀ m ≥ N,
    ε.Close (if h : n ≥ N then if h_1 : n ≥ n₀ then a ⟨n, ⋯⟩ else 0 else 0)
      (if h : m ≥ N then if h_1 : m ≥ n₀ then a ⟨m, ⋯⟩ else 0 else 0)⊢ k ≥ Nh.h.mpn₀:ℤa:{ n // n ≥ n₀ } → ℝε:ℝhε:ε > 0N:ℤhN:N ≥ n₀j:ℤhj:j ≥ Nk:ℤhk:k ≥ Nh':ε.Close (if h : j ≥ N then if h_1 : j ≥ n₀ then a ⟨j, ⋯⟩ else 0 else 0)
  (if h : k ≥ N then if h_1 : k ≥ n₀ then a ⟨k, ⋯⟩ else 0 else 0)⊢ dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε try omegaAll goals completed! 🐙
    simp_all [show n₀ ≤ j byn₀:ℤa:{ n // n ≥ n₀ } → ℝ⊢ (mk' n₀ a).IsCauchy ↔ ∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε omegaAll goals completed! 🐙, show n₀ ≤ k byn₀:ℤa:{ n // n ≥ n₀ } → ℝ⊢ (mk' n₀ a).IsCauchy ↔ ∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε omegaAll goals completed! 🐙]
  rintro ⟨ N, _, _ ⟩h.h.mprn₀:ℤa:{ n // n ≥ n₀ } → ℝε:ℝhε:ε > 0N:ℤleft✝:N ≥ n₀right✝:∀ j ≥ N, ∀ k ≥ N, dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε⊢ ε.EventuallySteady (mk' n₀ a); use max n₀ Nhn₀:ℤa:{ n // n ≥ n₀ } → ℝε:ℝhε:ε > 0N:ℤleft✝:N ≥ n₀right✝:∀ j ≥ N, ∀ k ≥ N, dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε⊢ max n₀ N ≥ (mk' n₀ a).m ∧ ε.Steady ((mk' n₀ a).from (max n₀ N)); grindAll goals completed! 🐙@[coe]
abbrev Sequence.ofChapter5Sequence (a: Chapter5.Sequence) : Sequence :=
{
  m := a.n₀
  seq n := a n
  vanish n hn := bya:Chapter5.Sequencen:ℤhn:n < a.n₀⊢ ↑(a.seq n) = 0 simp [a.vanish n hn]All goals completed! 🐙
}instance Chapter5.Sequence.inst_coe_sequence : Coe Chapter5.Sequence Sequence where
  coe := Sequence.ofChapter5Sequence@[simp]
theorem Chapter5.coe_sequence_eval (a: Chapter5.Sequence) (n:ℤ) : (a:Sequence) n = (a n:ℝ) := rfltheorem declaration uses `sorry`Sequence.is_steady_of_rat (ε:ℚ) (a: Chapter5.Sequence) :
    ε.Steady a ↔ (ε:ℝ).Steady (a:Sequence) := byε:ℚa:Chapter5.Sequence⊢ ε.Steady a ↔ (↑ε).Steady ↑a sorryAll goals completed! 🐙theorem declaration uses `sorry`Sequence.is_eventuallySteady_of_rat (ε:ℚ) (a: Chapter5.Sequence) :
    ε.EventuallySteady a ↔ (ε:ℝ).EventuallySteady (a:Sequence) := byε:ℚa:Chapter5.Sequence⊢ ε.EventuallySteady a ↔ (↑ε).EventuallySteady ↑a sorryAll goals completed! 🐙

Proposition 6.1.4

theorem Sequence.isCauchy_of_rat (a: Chapter5.Sequence) : a.IsCauchy ↔ (a:Sequence).IsCauchy := bya:Chapter5.Sequence⊢ a.IsCauchy ↔ (↑a).IsCauchy
  -- This proof is written to follow the structure of the original text.
  constructormpa:Chapter5.Sequence⊢ a.IsCauchy → (↑a).IsCauchympra:Chapter5.Sequence⊢ (↑a).IsCauchy → a.IsCauchy
  swapmpra:Chapter5.Sequence⊢ (↑a).IsCauchy → a.IsCauchympa:Chapter5.Sequence⊢ a.IsCauchy → (↑a).IsCauchy
  .mpra:Chapter5.Sequence⊢ (↑a).IsCauchy → a.IsCauchy intro hmpra:Chapter5.Sequenceh:(↑a).IsCauchy⊢ a.IsCauchy; rw [isCauchy_def] at hmpra:Chapter5.Sequenceh:∀ ε > 0, ε.EventuallySteady ↑a⊢ a.IsCauchy
    rw [Chapter5.Sequence.isCauchy_def]mpra:Chapter5.Sequenceh:∀ ε > 0, ε.EventuallySteady ↑a⊢ ∀ ε > 0, ε.EventuallySteady a
    intro ε hεmpra:Chapter5.Sequenceh:∀ ε > 0, ε.EventuallySteady ↑aε:ℚhε:ε > 0⊢ ε.EventuallySteady a
    specialize h ε (bya:Chapter5.Sequenceh:∀ ε > 0, ε.EventuallySteady ↑aε:ℚhε:ε > 0⊢ ↑ε > 0 positivityAll goals completed! 🐙)
    rwa [is_eventuallySteady_of_rat]mpra:Chapter5.Sequenceε:ℚhε:ε > 0h:(↑ε).EventuallySteady ↑a⊢ (↑ε).EventuallySteady ↑a
  intro hmpa:Chapter5.Sequenceh:a.IsCauchy⊢ (↑a).IsCauchy
  rw [Chapter5.Sequence.isCauchy_def] at hmpa:Chapter5.Sequenceh:∀ ε > 0, ε.EventuallySteady a⊢ (↑a).IsCauchy
  rw [isCauchy_def]mpa:Chapter5.Sequenceh:∀ ε > 0, ε.EventuallySteady a⊢ ∀ ε > 0, ε.EventuallySteady ↑a
  intro ε hεmpa:Chapter5.Sequenceh:∀ ε > 0, ε.EventuallySteady aε:ℝhε:ε > 0⊢ ε.EventuallySteady ↑a
  choose ε' hε' hlt using exists_pos_rat_lt hεmpa:Chapter5.Sequenceh:∀ ε > 0, ε.EventuallySteady aε:ℝhε:ε > 0ε':ℚhε':0 < ε'hlt:↑ε' < ε⊢ ε.EventuallySteady ↑a
  specialize h ε' hε'mpa:Chapter5.Sequenceε:ℝhε:ε > 0ε':ℚhε':0 < ε'hlt:↑ε' < εh:ε'.EventuallySteady a⊢ ε.EventuallySteady ↑a
  rw [is_eventuallySteady_of_rat] at hmpa:Chapter5.Sequenceε:ℝhε:ε > 0ε':ℚhε':0 < ε'hlt:↑ε' < εh:(↑ε').EventuallySteady ↑a⊢ ε.EventuallySteady ↑a
  exact h.mono (le_of_lt hlt)All goals completed! 🐙

end Chapter6

Definition 6.1.5 (CloseSeq)

abbrev Real.CloseSeq (ε: ℝ) (a: Chapter6.Sequence) (L:ℝ) : Prop := ∀ n ≥ a.m, ε.Close (a n) L

Definition 6.1.5 (CloseSeq, def)

theorem Real.closeSeq_def (ε: ℝ) (a: Chapter6.Sequence) (L:ℝ) :
  ε.CloseSeq a L ↔ ∀ n ≥ a.m, dist (a n) L ≤ ε := byε:ℝa:Chapter6.SequenceL:ℝ⊢ ε.CloseSeq a L ↔ ∀ n ≥ a.m, dist (a.seq n) L ≤ ε rflAll goals completed! 🐙

Definition 6.1.5 (EventuallyClose)

abbrev Real.EventuallyClose (ε: ℝ) (a: Chapter6.Sequence) (L:ℝ) : Prop :=
  ∃ N ≥ a.m, ε.CloseSeq (a.from N) L

Definition 6.1.5 (EventuallyClose, def)

theorem Real.eventuallyClose_def (ε: ℝ) (a: Chapter6.Sequence) (L:ℝ) :
  ε.EventuallyClose a L ↔ ∃ N, (N ≥ a.m) ∧ ε.CloseSeq (a.from N) L := byε:ℝa:Chapter6.SequenceL:ℝ⊢ ε.EventuallyClose a L ↔ ∃ N ≥ a.m, ε.CloseSeq (a.from N) L rflAll goals completed! 🐙

              theorem Real.CloseSeq.coe (ε : ℝ) (a : ℕ → ℝ) (L : ℝ):
  (ε.CloseSeq a L) ↔ ∀ n, dist (a n) L ≤ ε := byε:ℝa:ℕ → ℝL:ℝ⊢ ε.CloseSeq (↑a) L ↔ ∀ (n : ℕ), dist (a n) L ≤ ε
  constructormpε:ℝa:ℕ → ℝL:ℝ⊢ ε.CloseSeq (↑a) L → ∀ (n : ℕ), dist (a n) L ≤ εmprε:ℝa:ℕ → ℝL:ℝ⊢ (∀ (n : ℕ), dist (a n) L ≤ ε) → ε.CloseSeq (↑a) L
  .mpε:ℝa:ℕ → ℝL:ℝ⊢ ε.CloseSeq (↑a) L → ∀ (n : ℕ), dist (a n) L ≤ ε intro h nmpε:ℝa:ℕ → ℝL:ℝh:ε.CloseSeq (↑a) Ln:ℕ⊢ dist (a n) L ≤ ε; specialize h nmpε:ℝa:ℕ → ℝL:ℝn:ℕh:↑n ≥ (↑a).m → ε.Close ((↑a).seq ↑n) L⊢ dist (a n) L ≤ ε; grindAll goals completed! 🐙
  .mprε:ℝa:ℕ → ℝL:ℝ⊢ (∀ (n : ℕ), dist (a n) L ≤ ε) → ε.CloseSeq (↑a) L intro h nmprε:ℝa:ℕ → ℝL:ℝh:∀ (n : ℕ), dist (a n) L ≤ εn:ℤ⊢ n ≥ (↑a).m → ε.Close ((↑a).seq n) L hnmprε:ℝa:ℕ → ℝL:ℝh:∀ (n : ℕ), dist (a n) L ≤ εn:ℤhn:n ≥ (↑a).m⊢ ε.Close ((↑a).seq n) L; lift n to ℕ using (byε:ℝa:ℕ → ℝL:ℝh:∀ (n : ℕ), dist (a n) L ≤ εn:ℕhn:↑n ≥ (↑a).m⊢ ?m.48 omegaAll goals completed! 🐙); specialize h nmprε:ℝa:ℕ → ℝL:ℝn:ℕh:dist (a n) L ≤ ε⊢ ε.Close ((↑a).seq ↑n) L; grindAll goals completed! 🐙theorem Real.CloseSeq.mono {a: Chapter6.Sequence} {ε₁ ε₂ L: ℝ} (hε: ε₁ ≤ ε₂)
  (hclose: ε₁.CloseSeq a L) :
    ε₂.CloseSeq a L := bya:Chapter6.Sequenceε₁:ℝε₂:ℝL:ℝhε:ε₁ ≤ ε₂hclose:ε₁.CloseSeq a L⊢ ε₂.CloseSeq a L peel 2 hcloseh.ha:Chapter6.Sequenceε₁:ℝε₂:ℝL:ℝhε:ε₁ ≤ ε₂hclose:ε₁.CloseSeq a Ln✝:ℤa✝:n✝ ≥ a.mthis:ε₁.Close (a.seq n✝) L⊢ ε₂.Close (a.seq n✝) L; rw [Real.Close, Real.dist_eq] at *h.ha:Chapter6.Sequenceε₁:ℝε₂:ℝL:ℝhε:ε₁ ≤ ε₂hclose:ε₁.CloseSeq a Ln✝:ℤa✝:n✝ ≥ a.mthis:|a.seq n✝ - L| ≤ ε₁⊢ |a.seq n✝ - L| ≤ ε₂; linarithAll goals completed! 🐙theorem Real.EventuallyClose.mono {a: Chapter6.Sequence} {ε₁ ε₂ L: ℝ} (hε: ε₁ ≤ ε₂)
  (hclose: ε₁.EventuallyClose a L) :
    ε₂.EventuallyClose a L := bya:Chapter6.Sequenceε₁:ℝε₂:ℝL:ℝhε:ε₁ ≤ ε₂hclose:ε₁.EventuallyClose a L⊢ ε₂.EventuallyClose a L peel 2 hcloseh.ha:Chapter6.Sequenceε₁:ℝε₂:ℝL:ℝhε:ε₁ ≤ ε₂hclose:ε₁.EventuallyClose a LN✝:ℤp✝:N✝ ≥ a.mthis:ε₁.CloseSeq (a.from N✝) L⊢ ε₂.CloseSeq (a.from N✝) L; grind [CloseSeq.mono]All goals completed! 🐙namespace Chapter6abbrev Sequence.TendsTo (a:Sequence) (L:ℝ) : Prop :=
  ∀ ε > (0:ℝ), ε.EventuallyClose a Ltheorem Sequence.tendsTo_def (a:Sequence) (L:ℝ) :
  a.TendsTo L ↔ ∀ ε > (0:ℝ), ε.EventuallyClose a L := bya:SequenceL:ℝ⊢ a.TendsTo L ↔ ∀ ε > 0, ε.EventuallyClose a L rflAll goals completed! 🐙

Exercise 6.1.2

theorem declaration uses `sorry`Sequence.tendsTo_iff (a:Sequence) (L:ℝ) :
  a.TendsTo L ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, |a n - L| ≤ ε := bya:SequenceL:ℝ⊢ a.TendsTo L ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, |a.seq n - L| ≤ ε sorryAll goals completed! 🐙

              noncomputable def seq_6_1_6 : Sequence := (fun (n:ℕ) ↦ 1-(10:ℝ)^(-(n:ℤ)-1):Sequence)/-- Examples 6.1.6 (0.1 close) -/
example : (0.1:ℝ).CloseSeq seq_6_1_6 1 := by⊢ Real.CloseSeq 0.1 seq_6_1_6 1
  rw [seq_6_1_6, Real.CloseSeq.coe]⊢ ∀ (n : ℕ), dist (1 - 10 ^ (-↑n - 1)) 1 ≤ 0.1
  intro nn:ℕ⊢ dist (1 - 10 ^ (-↑n - 1)) 1 ≤ 0.1
  rw [Real.dist_eq, abs_sub_comm, abs_of_nonneg (by
    rw [sub_nonneg]
    rw (occs := .pos [2]) [show (1:ℝ) = 1 - 0 by norm_num]
    gcongr
    positivity
  ), sub_sub_cancel, show (0.1:ℝ) = (10:ℝ)^(-1:ℤ) by norm_num]n:ℕ⊢ 10 ^ (-↑n - 1) ≤ 10 ^ (-1)
  gcongrhan:ℕ⊢ 1 ≤ 10hmnn:ℕ⊢ -↑n - 1 ≤ -1 <;>han:ℕ⊢ 1 ≤ 10hmnn:ℕ⊢ -↑n - 1 ≤ -1 grindAll goals completed! 🐙/-- Examples 6.1.6 (0.01 not close) -/
example : ¬ (0.01:ℝ).CloseSeq seq_6_1_6 1 := by⊢ ¬Real.CloseSeq 1e-2 seq_6_1_6 1
  intro hh:Real.CloseSeq 1e-2 seq_6_1_6 1⊢ False; specialize h 0 (byh:Real.CloseSeq 1e-2 seq_6_1_6 1⊢ 0 ≥ seq_6_1_6.m positivityAll goals completed! 🐙); simp [seq_6_1_6] at hh:10⁻¹ ≤ 1e-2⊢ False; norm_num at hAll goals completed! 🐙/-- Examples 6.1.6 (0.01 eventually close) -/
declaration uses `sorry`example : (0.01:ℝ).EventuallyClose seq_6_1_6 1 := by⊢ Real.EventuallyClose 1e-2 seq_6_1_6 1 sorryAll goals completed! 🐙/-- Examples 6.1.6 (tends to 1) -/
declaration uses `sorry`example : seq_6_1_6.TendsTo 1 := by⊢ seq_6_1_6.TendsTo 1 sorryAll goals completed! 🐙

Proposition 6.1.7 (Uniqueness of limits)

theorem Sequence.tendsTo_unique (a:Sequence) {L L':ℝ} (h:L ≠ L') :
    ¬ (a.TendsTo L ∧ a.TendsTo L') := bya:SequenceL:ℝL':ℝh:L ≠ L'⊢ ¬(a.TendsTo L ∧ a.TendsTo L')
  -- This proof is written to follow the structure of the original text.
  by_contra thisa:SequenceL:ℝL':ℝh:L ≠ L'this:a.TendsTo L ∧ a.TendsTo L'⊢ False
  choose hL hL' using thisa:SequenceL:ℝL':ℝh:L ≠ L'hL:a.TendsTo LhL':a.TendsTo L'⊢ False
  replace h : L - L' ≠ 0 := bya:SequenceL:ℝL':ℝh:L ≠ L'⊢ ¬(a.TendsTo L ∧ a.TendsTo L') grindAll goals completed! 🐙
  replace h : |L-L'| > 0 := bya:SequenceL:ℝL':ℝh:L ≠ L'⊢ ¬(a.TendsTo L ∧ a.TendsTo L') positivityAll goals completed! 🐙
  set ε := |L-L'| / 3a:SequenceL:ℝL':ℝhL:a.TendsTo LhL':a.TendsTo L'h:|L - L'| > 0ε:ℝ := |L - L'| / 3⊢ False
  have hε : ε > 0 := bya:SequenceL:ℝL':ℝh:L ≠ L'⊢ ¬(a.TendsTo L ∧ a.TendsTo L') positivityAll goals completed! 🐙
  rw [tendsTo_iff] at hL hL'a:SequenceL:ℝL':ℝhL:∀ ε > 0, ∃ N, ∀ n ≥ N, |a.seq n - L| ≤ εhL':∀ ε > 0, ∃ N, ∀ n ≥ N, |a.seq n - L'| ≤ εh:|L - L'| > 0ε:ℝ := |L - L'| / 3hε:ε > 0⊢ False
  specialize hL ε hεa:SequenceL:ℝL':ℝhL':∀ ε > 0, ∃ N, ∀ n ≥ N, |a.seq n - L'| ≤ εh:|L - L'| > 0ε:ℝ := |L - L'| / 3hε:ε > 0hL:∃ N, ∀ n ≥ N, |a.seq n - L| ≤ ε⊢ False; choose N hN using hLa:SequenceL:ℝL':ℝhL':∀ ε > 0, ∃ N, ∀ n ≥ N, |a.seq n - L'| ≤ εh:|L - L'| > 0ε:ℝ := |L - L'| / 3hε:ε > 0N:ℤhN:∀ n ≥ N, |a.seq n - L| ≤ ε⊢ False
  specialize hL' ε hεa:SequenceL:ℝL':ℝh:|L - L'| > 0ε:ℝ := |L - L'| / 3hε:ε > 0N:ℤhN:∀ n ≥ N, |a.seq n - L| ≤ εhL':∃ N, ∀ n ≥ N, |a.seq n - L'| ≤ ε⊢ False; choose M hM using hL'a:SequenceL:ℝL':ℝh:|L - L'| > 0ε:ℝ := |L - L'| / 3hε:ε > 0N:ℤhN:∀ n ≥ N, |a.seq n - L| ≤ εM:ℤhM:∀ n ≥ M, |a.seq n - L'| ≤ ε⊢ False
  set n := max N Ma:SequenceL:ℝL':ℝh:|L - L'| > 0ε:ℝ := |L - L'| / 3hε:ε > 0N:ℤhN:∀ n ≥ N, |a.seq n - L| ≤ εM:ℤhM:∀ n ≥ M, |a.seq n - L'| ≤ εn:ℤ := max N M⊢ False
  specialize hN n (bya:SequenceL:ℝL':ℝh:|L - L'| > 0ε:ℝ := |L - L'| / 3hε:ε > 0N:ℤhN:∀ n ≥ N, |a.seq n - L| ≤ εM:ℤhM:∀ n ≥ M, |a.seq n - L'| ≤ εn:ℤ := max N M⊢ n ≥ N omegaAll goals completed! 🐙)
  specialize hM n (bya:SequenceL:ℝL':ℝh:|L - L'| > 0ε:ℝ := |L - L'| / 3hε:ε > 0N:ℤM:ℤhM:∀ n ≥ M, |a.seq n - L'| ≤ εn:ℤ := max N MhN:|a.seq n - L| ≤ ε⊢ n ≥ M omegaAll goals completed! 🐙)
  have : |L-L'| ≤ 2 * |L-L'|/3 := calc
    _ = dist L L' := bya:SequenceL:ℝL':ℝh:|L - L'| > 0ε:ℝ := |L - L'| / 3hε:ε > 0N:ℤM:ℤn:ℤ := max N MhN:|a.seq n - L| ≤ εhM:|a.seq n - L'| ≤ ε⊢ |L - L'| = dist L L' rw [Real.dist_eq]All goals completed! 🐙
    _ ≤ dist L (a.seq n) + dist (a.seq n) L' := dist_triangle _ _ _
    _ ≤ ε + ε := bya:SequenceL:ℝL':ℝh:|L - L'| > 0ε:ℝ := |L - L'| / 3hε:ε > 0N:ℤM:ℤn:ℤ := max N MhN:|a.seq n - L| ≤ εhM:|a.seq n - L'| ≤ ε⊢ dist L (a.seq n) + dist (a.seq n) L' ≤ ε + ε rw [←Real.dist_eq] at hN hMa:SequenceL:ℝL':ℝh:|L - L'| > 0ε:ℝ := |L - L'| / 3hε:ε > 0N:ℤM:ℤn:ℤ := max N MhN:dist (a.seq n) L ≤ εhM:dist (a.seq n) L' ≤ ε⊢ dist L (a.seq n) + dist (a.seq n) L' ≤ ε + ε; rw [dist_comm] at hNa:SequenceL:ℝL':ℝh:|L - L'| > 0ε:ℝ := |L - L'| / 3hε:ε > 0N:ℤM:ℤn:ℤ := max N MhN:dist L (a.seq n) ≤ εhM:dist (a.seq n) L' ≤ ε⊢ dist L (a.seq n) + dist (a.seq n) L' ≤ ε + ε; gcongrAll goals completed! 🐙
    _ = 2 * |L-L'|/3 := bya:SequenceL:ℝL':ℝh:|L - L'| > 0ε:ℝ := |L - L'| / 3hε:ε > 0N:ℤM:ℤn:ℤ := max N MhN:|a.seq n - L| ≤ εhM:|a.seq n - L'| ≤ ε⊢ ε + ε = 2 * |L - L'| / 3 grindAll goals completed! 🐙
  linarithAll goals completed! 🐙

Definition 6.1.8 (Convergent)

abbrev Sequence.Convergent (a:Sequence) : Prop := ∃ L, a.TendsTo L

Definition 6.1.8 (Convergent, def)

theorem Sequence.convergent_def (a:Sequence) : a.Convergent ↔ ∃ L, a.TendsTo L := bya:Sequence⊢ a.Convergent ↔ ∃ L, a.TendsTo L rflAll goals completed! 🐙

Definition 6.1.8 (Divergent)

abbrev Sequence.Divergent (a:Sequence) : Prop := ¬ a.Convergent

Definition 6.1.8 (Divergent, def)

theorem Sequence.divergent_def (a:Sequence) : a.Divergent ↔ ¬ a.Convergent := bya:Sequence⊢ a.Divergent ↔ ¬a.Convergent rflAll goals completed! 🐙

Definition 6.1.8. We give the limit of a sequence the junk value of 0 if it is not convergent.

open Classical innoncomputable abbrev lim (a:Sequence) : ℝ := if h: a.Convergent then h.choose else 0

Definition 6.1.8 (lim, def)

theorem Sequence.lim_def {a:Sequence} (h: a.Convergent) : a.TendsTo (lim a) := bya:Sequenceh:a.Convergent⊢ a.TendsTo (lim a)
  simp [lim, h]a:Sequenceh:a.Convergent⊢ a.TendsTo (Exists.choose ⋯); exact h.choose_specAll goals completed! 🐙

Definition 6.1.8 (lim, characterization)

theorem Sequence.lim_eq {a:Sequence} {L:ℝ} :
a.TendsTo L ↔ a.Convergent ∧ lim a = L := bya:SequenceL:ℝ⊢ a.TendsTo L ↔ a.Convergent ∧ lim a = L
  constructormpa:SequenceL:ℝ⊢ a.TendsTo L → a.Convergent ∧ lim a = Lmpra:SequenceL:ℝ⊢ a.Convergent ∧ lim a = L → a.TendsTo L
  .mpa:SequenceL:ℝ⊢ a.TendsTo L → a.Convergent ∧ lim a = L intro hmpa:SequenceL:ℝh:a.TendsTo L⊢ a.Convergent ∧ lim a = L; by_contra! eqmpa:SequenceL:ℝh:a.TendsTo Leq:a.Convergent → lim a ≠ L⊢ False
    have : a.Convergent := bya:SequenceL:ℝ⊢ a.TendsTo L ↔ a.Convergent ∧ lim a = L rw [convergent_def]a:SequenceL:ℝh:a.TendsTo Leq:a.Convergent → lim a ≠ L⊢ ∃ L, a.TendsTo L; use LAll goals completed! 🐙
    replace eq := a.tendsTo_unique (eq this)mpa:SequenceL:ℝh:a.TendsTo Lthis:a.Convergenteq:¬(a.TendsTo (lim a) ∧ a.TendsTo L)⊢ False
    apply lim_def at thismpa:SequenceL:ℝh:a.TendsTo Leq:¬(a.TendsTo (lim a) ∧ a.TendsTo L)this:a.TendsTo (lim a)⊢ False; tautoAll goals completed! 🐙
  intro ⟨ h, rfl ⟩mpra:SequenceL:ℝh:a.Convergent⊢ a.TendsTo (lim a); convert lim_def hAll goals completed! 🐙

Proposition 6.1.11

theorem Sequence.lim_harmonic :
    ((fun (n:ℕ) ↦ (n+1:ℝ)⁻¹):Sequence).Convergent ∧ lim ((fun (n:ℕ) ↦ (n+1:ℝ)⁻¹):Sequence) = 0 := by⊢ (↑fun n ↦ (↑n + 1)⁻¹).Convergent ∧ (lim ↑fun n ↦ (↑n + 1)⁻¹) = 0
  -- This proof is written to follow the structure of the original text.
  rw [←lim_eq, tendsTo_iff]⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, |(↑fun n ↦ (↑n + 1)⁻¹).seq n - 0| ≤ ε
  intro ε hεε:ℝhε:ε > 0⊢ ∃ N, ∀ n ≥ N, |(↑fun n ↦ (↑n + 1)⁻¹).seq n - 0| ≤ ε
  choose N hN using exists_int_gt (1 / ε)ε:ℝhε:ε > 0N:ℤhN:1 / ε < ↑N⊢ ∃ N, ∀ n ≥ N, |(↑fun n ↦ (↑n + 1)⁻¹).seq n - 0| ≤ ε; use Nhε:ℝhε:ε > 0N:ℤhN:1 / ε < ↑N⊢ ∀ n ≥ N, |(↑fun n ↦ (↑n + 1)⁻¹).seq n - 0| ≤ ε; intro n hnhε:ℝhε:ε > 0N:ℤhN:1 / ε < ↑Nn:ℤhn:n ≥ N⊢ |(↑fun n ↦ (↑n + 1)⁻¹).seq n - 0| ≤ ε
  have hNpos : (N:ℝ) > 0 := by⊢ (↑fun n ↦ (↑n + 1)⁻¹).Convergent ∧ (lim ↑fun n ↦ (↑n + 1)⁻¹) = 0 apply LT.lt.trans _ hNε:ℝhε:ε > 0N:ℤhN:1 / ε < ↑Nn:ℤhn:n ≥ N⊢ 0 < 1 / ε; positivityAll goals completed! 🐙
  simp at hNposhε:ℝhε:ε > 0N:ℤhN:1 / ε < ↑Nn:ℤhn:n ≥ NhNpos:0 < N⊢ |(↑fun n ↦ (↑n + 1)⁻¹).seq n - 0| ≤ ε
  have hnpos : n ≥ 0 := by⊢ (↑fun n ↦ (↑n + 1)⁻¹).Convergent ∧ (lim ↑fun n ↦ (↑n + 1)⁻¹) = 0 linarithAll goals completed! 🐙
  simp [hnpos, abs_inv]hε:ℝhε:ε > 0N:ℤhN:1 / ε < ↑Nn:ℤhn:n ≥ NhNpos:0 < Nhnpos:n ≥ 0⊢ |↑n.toNat + 1|⁻¹ ≤ ε
  calc
    _ ≤ (N:ℝ)⁻¹ := byε:ℝhε:ε > 0N:ℤhN:1 / ε < ↑Nn:ℤhn:n ≥ NhNpos:0 < Nhnpos:n ≥ 0⊢ |↑n.toNat + 1|⁻¹ ≤ (↑N)⁻¹
      rw [inv_le_inv₀]ε:ℝhε:ε > 0N:ℤhN:1 / ε < ↑Nn:ℤhn:n ≥ NhNpos:0 < Nhnpos:n ≥ 0⊢ ↑N ≤ |↑n.toNat + 1|haε:ℝhε:ε > 0N:ℤhN:1 / ε < ↑Nn:ℤhn:n ≥ NhNpos:0 < Nhnpos:n ≥ 0⊢ 0 < |↑n.toNat + 1|hbε:ℝhε:ε > 0N:ℤhN:1 / ε < ↑Nn:ℤhn:n ≥ NhNpos:0 < Nhnpos:n ≥ 0⊢ 0 < ↑N <;>ε:ℝhε:ε > 0N:ℤhN:1 / ε < ↑Nn:ℤhn:n ≥ NhNpos:0 < Nhnpos:n ≥ 0⊢ ↑N ≤ |↑n.toNat + 1|haε:ℝhε:ε > 0N:ℤhN:1 / ε < ↑Nn:ℤhn:n ≥ NhNpos:0 < Nhnpos:n ≥ 0⊢ 0 < |↑n.toNat + 1|hbε:ℝhε:ε > 0N:ℤhN:1 / ε < ↑Nn:ℤhn:n ≥ NhNpos:0 < Nhnpos:n ≥ 0⊢ 0 < ↑N try positivityAll goals completed! 🐙
      calc
        _ ≤ (n:ℝ) := byε:ℝhε:ε > 0N:ℤhN:1 / ε < ↑Nn:ℤhn:n ≥ NhNpos:0 < Nhnpos:n ≥ 0⊢ ↑N ≤ ↑n simp [hn]All goals completed! 🐙
        _ = (n.toNat:ℤ) := byε:ℝhε:ε > 0N:ℤhN:1 / ε < ↑Nn:ℤhn:n ≥ NhNpos:0 < Nhnpos:n ≥ 0⊢ ↑n = ↑↑n.toNat simp [hnpos]All goals completed! 🐙
        _ = n.toNat := rfl
        _ ≤ (n.toNat:ℝ) + 1 := byε:ℝhε:ε > 0N:ℤhN:1 / ε < ↑Nn:ℤhn:n ≥ NhNpos:0 < Nhnpos:n ≥ 0⊢ ↑n.toNat ≤ ↑n.toNat + 1 linarithAll goals completed! 🐙
        _ ≤ _ := le_abs_self _
    _ ≤ ε := byε:ℝhε:ε > 0N:ℤhN:1 / ε < ↑Nn:ℤhn:n ≥ NhNpos:0 < Nhnpos:n ≥ 0⊢ (↑N)⁻¹ ≤ ε
      rw [inv_le_comm₀]ε:ℝhε:ε > 0N:ℤhN:1 / ε < ↑Nn:ℤhn:n ≥ NhNpos:0 < Nhnpos:n ≥ 0⊢ ε⁻¹ ≤ ↑Nhaε:ℝhε:ε > 0N:ℤhN:1 / ε < ↑Nn:ℤhn:n ≥ NhNpos:0 < Nhnpos:n ≥ 0⊢ 0 < ↑Nhbε:ℝhε:ε > 0N:ℤhN:1 / ε < ↑Nn:ℤhn:n ≥ NhNpos:0 < Nhnpos:n ≥ 0⊢ 0 < ε <;>ε:ℝhε:ε > 0N:ℤhN:1 / ε < ↑Nn:ℤhn:n ≥ NhNpos:0 < Nhnpos:n ≥ 0⊢ ε⁻¹ ≤ ↑Nhaε:ℝhε:ε > 0N:ℤhN:1 / ε < ↑Nn:ℤhn:n ≥ NhNpos:0 < Nhnpos:n ≥ 0⊢ 0 < ↑Nhbε:ℝhε:ε > 0N:ℤhN:1 / ε < ↑Nn:ℤhn:n ≥ NhNpos:0 < Nhnpos:n ≥ 0⊢ 0 < ε try positivityAll goals completed! 🐙
      rw [←inv_eq_one_div _] at hNε:ℝhε:ε > 0N:ℤhN:ε⁻¹ < ↑Nn:ℤhn:n ≥ NhNpos:0 < Nhnpos:n ≥ 0⊢ ε⁻¹ ≤ ↑N; orderAll goals completed! 🐙

Proposition 6.1.12 / Exercise 6.1.5

theorem declaration uses `sorry`Sequence.IsCauchy.convergent {a:Sequence} (h:a.Convergent) : a.IsCauchy := bya:Sequenceh:a.Convergent⊢ a.IsCauchy
  sorryAll goals completed! 🐙

              /-- Example 6.1.13 (not eventually steady) -/
declaration uses `sorry`example : ¬ (0.1:ℝ).EventuallySteady ((fun n ↦ (-1:ℝ)^n):Sequence) := by⊢ ¬Real.EventuallySteady 0.1 ↑fun n ↦ (-1) ^ n sorryAll goals completed! 🐙/-- Example 6.1.13 (not Cauchy) -/
declaration uses `sorry`example : ¬ ((fun n ↦ (-1:ℝ)^n):Sequence).IsCauchy := by⊢ ¬(↑fun n ↦ (-1) ^ n).IsCauchy sorryAll goals completed! 🐙/-- Example 6.1.13 (not convergent) -/
declaration uses `sorry`example : ¬ ((fun n ↦ (-1:ℝ)^n):Sequence).Convergent := by⊢ ¬(↑fun n ↦ (-1) ^ n).Convergent sorryAll goals completed! 🐙

Proposition 6.1.15 / Exercise 6.1.6 (Formal limits are genuine limits)

theorem declaration uses `sorry`Sequence.lim_eq_LIM {a:ℕ → ℚ} (h: (a:Chapter5.Sequence).IsCauchy) :
    ((a:Chapter5.Sequence):Sequence).TendsTo (Chapter5.Real.equivR (Chapter5.LIM a)) := bya:ℕ → ℚh:(↑a).IsCauchy⊢ (↑↑a).TendsTo (Chapter5.Real.equivR (Chapter5.LIM a)) sorryAll goals completed! 🐙

Definition 6.1.16 (BoundedBy)

abbrev Sequence.BoundedBy (a:Sequence) (M:ℝ) : Prop :=
  ∀ n, |a n| ≤ M

Definition 6.1.16 (BoundedBy, def)

lemma Sequence.boundedBy_def (a:Sequence) (M:ℝ) :
  a.BoundedBy M ↔ ∀ n, |a n| ≤ M := bya:SequenceM:ℝ⊢ a.BoundedBy M ↔ ∀ (n : ℤ), |a.seq n| ≤ M rflAll goals completed! 🐙

Definition 6.1.16 (IsBounded)

abbrev Sequence.IsBounded (a:Sequence) : Prop := ∃ M ≥ 0, a.BoundedBy M

Definition 6.1.16 (IsBounded, def)

lemma Sequence.isBounded_def (a:Sequence) :
  a.IsBounded ↔ ∃ M ≥ 0, a.BoundedBy M := bya:Sequence⊢ a.IsBounded ↔ ∃ M ≥ 0, a.BoundedBy M rflAll goals completed! 🐙

theorem declaration uses `sorry`Sequence.bounded_of_cauchy {a:Sequence} (h: a.IsCauchy) : a.IsBounded := bya:Sequenceh:a.IsCauchy⊢ a.IsBounded
  sorryAll goals completed! 🐙

Corollary 6.1.17

theorem declaration uses `sorry`Sequence.bounded_of_convergent {a:Sequence} (h: a.Convergent) : a.IsBounded := bya:Sequenceh:a.Convergent⊢ a.IsBounded
  sorryAll goals completed! 🐙

              /-- Example 6.1.18 (not bounded) -/
declaration uses `sorry`example : ¬ ((fun (n:ℕ) ↦ (n+1:ℝ)):Sequence).IsBounded := by⊢ ¬(↑fun n ↦ ↑n + 1).IsBounded sorryAll goals completed! 🐙/-- Example 6.1.18 (not convergent) -/
declaration uses `sorry`example : ¬ ((fun (n:ℕ) ↦ (n+1:ℝ)):Sequence).Convergent := by⊢ ¬(↑fun n ↦ ↑n + 1).Convergent sorryAll goals completed! 🐙instance Sequence.inst_add : Add Sequence where
  add a b := {
    m := min a.m b.m
    seq n := a n + b n
    vanish n hn := bya:Sequenceb:Sequencen:ℤhn:n < min a.m b.m⊢ a.seq n + b.seq n = 0 simp [a.vanish n (by grind), b.vanish n (by grind)]All goals completed! 🐙
  }@[simp]
theorem Sequence.add_eval {a b: Sequence} (n:ℤ) : (a + b) n = a n + b n := rfltheorem Sequence.add_coe (a b: ℕ → ℝ) : (a:Sequence) + (b:Sequence) = (fun n ↦ a n + b n) := bya:ℕ → ℝb:ℕ → ℝ⊢ ↑a + ↑b = ↑fun n ↦ a n + b n
  ext nma:ℕ → ℝb:ℕ → ℝ⊢ (↑a + ↑b).m = (↑fun n ↦ a n + b n).mseq.ha:ℕ → ℝb:ℕ → ℝn:ℤ⊢ (↑a + ↑b).seq n = (↑fun n ↦ a n + b n).seq n; rflseq.ha:ℕ → ℝb:ℕ → ℝn:ℤ⊢ (↑a + ↑b).seq n = (↑fun n ↦ a n + b n).seq n
  by_cases h:n ≥ 0posa:ℕ → ℝb:ℕ → ℝn:ℤh:n ≥ 0⊢ (↑a + ↑b).seq n = (↑fun n ↦ a n + b n).seq nnega:ℕ → ℝb:ℕ → ℝn:ℤh:¬n ≥ 0⊢ (↑a + ↑b).seq n = (↑fun n ↦ a n + b n).seq n <;>posa:ℕ → ℝb:ℕ → ℝn:ℤh:n ≥ 0⊢ (↑a + ↑b).seq n = (↑fun n ↦ a n + b n).seq nnega:ℕ → ℝb:ℕ → ℝn:ℤh:¬n ≥ 0⊢ (↑a + ↑b).seq n = (↑fun n ↦ a n + b n).seq n simp [h]All goals completed! 🐙

Theorem 6.1.19(a) (limit laws). The Sequence.TendsTo version is more usable than the lim version in applications.

theorem declaration uses `sorry`Sequence.tendsTo_add {a b:Sequence} {L M:ℝ} (ha: a.TendsTo L) (hb: b.TendsTo M) :
  (a+b).TendsTo (L+M) := bya:Sequenceb:SequenceL:ℝM:ℝha:a.TendsTo Lhb:b.TendsTo M⊢ (a + b).TendsTo (L + M)
  sorryAll goals completed! 🐙

              theorem declaration uses `sorry`Sequence.lim_add {a b:Sequence} (ha: a.Convergent) (hb: b.Convergent) :
  (a + b).Convergent ∧ lim (a + b) = lim a + lim b := bya:Sequenceb:Sequenceha:a.Convergenthb:b.Convergent⊢ (a + b).Convergent ∧ lim (a + b) = lim a + lim b
  sorryAll goals completed! 🐙instance Sequence.inst_mul : Mul Sequence where
  mul a b := {
    m := min a.m b.m
    seq n := a n * b n
    vanish n hn := bya:Sequenceb:Sequencen:ℤhn:n < min a.m b.m⊢ a.seq n * b.seq n = 0 simp [a.vanish n (by grind), b.vanish n (by grind)]All goals completed! 🐙
  }@[simp]
theorem Sequence.mul_eval {a b: Sequence} (n:ℤ) : (a * b) n = a n * b n := rfltheorem Sequence.mul_coe (a b: ℕ → ℝ) : (a:Sequence) * (b:Sequence) = (fun n ↦ a n * b n) := bya:ℕ → ℝb:ℕ → ℝ⊢ ↑a * ↑b = ↑fun n ↦ a n * b n
  ext nma:ℕ → ℝb:ℕ → ℝ⊢ (↑a * ↑b).m = (↑fun n ↦ a n * b n).mseq.ha:ℕ → ℝb:ℕ → ℝn:ℤ⊢ (↑a * ↑b).seq n = (↑fun n ↦ a n * b n).seq n; rflseq.ha:ℕ → ℝb:ℕ → ℝn:ℤ⊢ (↑a * ↑b).seq n = (↑fun n ↦ a n * b n).seq n
  by_cases h:n ≥ 0posa:ℕ → ℝb:ℕ → ℝn:ℤh:n ≥ 0⊢ (↑a * ↑b).seq n = (↑fun n ↦ a n * b n).seq nnega:ℕ → ℝb:ℕ → ℝn:ℤh:¬n ≥ 0⊢ (↑a * ↑b).seq n = (↑fun n ↦ a n * b n).seq n <;>posa:ℕ → ℝb:ℕ → ℝn:ℤh:n ≥ 0⊢ (↑a * ↑b).seq n = (↑fun n ↦ a n * b n).seq nnega:ℕ → ℝb:ℕ → ℝn:ℤh:¬n ≥ 0⊢ (↑a * ↑b).seq n = (↑fun n ↦ a n * b n).seq n simp [h]All goals completed! 🐙

Theorem 6.1.19(b) (limit laws). The Sequence.TendsTo version is more usable than the lim version in applications.

theorem declaration uses `sorry`Sequence.tendsTo_mul {a b:Sequence} {L M:ℝ} (ha: a.TendsTo L) (hb: b.TendsTo M) :
    (a * b).TendsTo (L * M) := bya:Sequenceb:SequenceL:ℝM:ℝha:a.TendsTo Lhb:b.TendsTo M⊢ (a * b).TendsTo (L * M)
  sorryAll goals completed! 🐙

              theorem declaration uses `sorry`Sequence.lim_mul {a b:Sequence} (ha: a.Convergent) (hb: b.Convergent) :
    (a * b).Convergent ∧ lim (a * b) = lim a * lim b := bya:Sequenceb:Sequenceha:a.Convergenthb:b.Convergent⊢ (a * b).Convergent ∧ lim (a * b) = lim a * lim b
  sorryAll goals completed! 🐙instance Sequence.inst_smul : SMul ℝ Sequence where
  smul c a := {
    m := a.m
    seq n := c * a n
    vanish n hn := byc:ℝa:Sequencen:ℤhn:n < a.m⊢ c * a.seq n = 0 simp [a.vanish n hn]All goals completed! 🐙
  }@[simp]
theorem Sequence.smul_eval {a: Sequence} (c: ℝ) (n:ℤ) : (c • a) n = c * a n := rfltheorem Sequence.smul_coe (c:ℝ) (a:ℕ → ℝ) : (c • (a:Sequence)) = (fun n ↦ c * a n) := byc:ℝa:ℕ → ℝ⊢ c • ↑a = ↑fun n ↦ c * a n
  ext nmc:ℝa:ℕ → ℝ⊢ (c • ↑a).m = (↑fun n ↦ c * a n).mseq.hc:ℝa:ℕ → ℝn:ℤ⊢ (c • ↑a).seq n = (↑fun n ↦ c * a n).seq n; rflseq.hc:ℝa:ℕ → ℝn:ℤ⊢ (c • ↑a).seq n = (↑fun n ↦ c * a n).seq n
  by_cases h:n ≥ 0posc:ℝa:ℕ → ℝn:ℤh:n ≥ 0⊢ (c • ↑a).seq n = (↑fun n ↦ c * a n).seq nnegc:ℝa:ℕ → ℝn:ℤh:¬n ≥ 0⊢ (c • ↑a).seq n = (↑fun n ↦ c * a n).seq n <;>posc:ℝa:ℕ → ℝn:ℤh:n ≥ 0⊢ (c • ↑a).seq n = (↑fun n ↦ c * a n).seq nnegc:ℝa:ℕ → ℝn:ℤh:¬n ≥ 0⊢ (c • ↑a).seq n = (↑fun n ↦ c * a n).seq n simp [h, HSMul.hSMul, SMul.smul]All goals completed! 🐙

Theorem 6.1.19(c) (limit laws). The Sequence.TendsTo version is more usable than the lim version in applications.

theorem declaration uses `sorry`Sequence.tendsTo_smul (c:ℝ) {a:Sequence} {L:ℝ} (ha: a.TendsTo L) :
    (c • a).TendsTo (c * L) := byc:ℝa:SequenceL:ℝha:a.TendsTo L⊢ (c • a).TendsTo (c * L)
  sorryAll goals completed! 🐙

              theorem declaration uses `sorry`Sequence.lim_smul (c:ℝ) {a:Sequence} (ha: a.Convergent) :
    (c • a).Convergent ∧ lim (c • a) = c * lim a := byc:ℝa:Sequenceha:a.Convergent⊢ (c • a).Convergent ∧ lim (c • a) = c * lim a
  sorryAll goals completed! 🐙instance Sequence.inst_sub : Sub Sequence where
  sub a b := {
    m := min a.m b.m
    seq n := a n - b n
    vanish n hn := bya:Sequenceb:Sequencen:ℤhn:n < min a.m b.m⊢ a.seq n - b.seq n = 0 simp [a.vanish n (by grind), b.vanish n (by grind)]All goals completed! 🐙
  }@[simp]
theorem Sequence.sub_eval {a b: Sequence} (n:ℤ) : (a - b) n = a n - b n := rfltheorem Sequence.sub_coe (a b: ℕ → ℝ) : (a:Sequence) - (b:Sequence) = (fun n ↦ a n - b n) := bya:ℕ → ℝb:ℕ → ℝ⊢ ↑a - ↑b = ↑fun n ↦ a n - b n
  ext nma:ℕ → ℝb:ℕ → ℝ⊢ (↑a - ↑b).m = (↑fun n ↦ a n - b n).mseq.ha:ℕ → ℝb:ℕ → ℝn:ℤ⊢ (↑a - ↑b).seq n = (↑fun n ↦ a n - b n).seq n; rflseq.ha:ℕ → ℝb:ℕ → ℝn:ℤ⊢ (↑a - ↑b).seq n = (↑fun n ↦ a n - b n).seq n
  by_cases h:n ≥ 0posa:ℕ → ℝb:ℕ → ℝn:ℤh:n ≥ 0⊢ (↑a - ↑b).seq n = (↑fun n ↦ a n - b n).seq nnega:ℕ → ℝb:ℕ → ℝn:ℤh:¬n ≥ 0⊢ (↑a - ↑b).seq n = (↑fun n ↦ a n - b n).seq n <;>posa:ℕ → ℝb:ℕ → ℝn:ℤh:n ≥ 0⊢ (↑a - ↑b).seq n = (↑fun n ↦ a n - b n).seq nnega:ℕ → ℝb:ℕ → ℝn:ℤh:¬n ≥ 0⊢ (↑a - ↑b).seq n = (↑fun n ↦ a n - b n).seq n simp [h]All goals completed! 🐙

Theorem 6.1.19(d) (limit laws). The Sequence.TendsTo version is more usable than the lim version in applications.

theorem declaration uses `sorry`Sequence.tendsTo_sub {a b:Sequence} {L M:ℝ} (ha: a.TendsTo L) (hb: b.TendsTo M) :
    (a - b).TendsTo (L - M) := bya:Sequenceb:SequenceL:ℝM:ℝha:a.TendsTo Lhb:b.TendsTo M⊢ (a - b).TendsTo (L - M)
  sorryAll goals completed! 🐙

              theorem declaration uses `sorry`Sequence.LIM_sub {a b:Sequence} (ha: a.Convergent) (hb: b.Convergent) :
    (a - b).Convergent ∧ lim (a - b) = lim a - lim b := bya:Sequenceb:Sequenceha:a.Convergenthb:b.Convergent⊢ (a - b).Convergent ∧ lim (a - b) = lim a - lim b
  sorryAll goals completed! 🐙noncomputable instance Sequence.inst_inv : Inv Sequence where
  inv a := {
    m := a.m
    seq n := (a n)⁻¹
    vanish n hn := bya:Sequencen:ℤhn:n < a.m⊢ (a.seq n)⁻¹ = 0 simp [a.vanish n hn]All goals completed! 🐙
  }@[simp]
theorem Sequence.inv_eval {a: Sequence} (n:ℤ) : (a⁻¹) n = (a n)⁻¹ := rfltheorem Sequence.inv_coe (a: ℕ → ℝ) : (a:Sequence)⁻¹ = (fun n ↦ (a n)⁻¹) := bya:ℕ → ℝ⊢ (↑a)⁻¹ = ↑fun n ↦ (a n)⁻¹
  ext nma:ℕ → ℝ⊢ (↑a)⁻¹.m = (↑fun n ↦ (a n)⁻¹).mseq.ha:ℕ → ℝn:ℤ⊢ (↑a)⁻¹.seq n = (↑fun n ↦ (a n)⁻¹).seq n; rflseq.ha:ℕ → ℝn:ℤ⊢ (↑a)⁻¹.seq n = (↑fun n ↦ (a n)⁻¹).seq n
  by_cases h:n ≥ 0posa:ℕ → ℝn:ℤh:n ≥ 0⊢ (↑a)⁻¹.seq n = (↑fun n ↦ (a n)⁻¹).seq nnega:ℕ → ℝn:ℤh:¬n ≥ 0⊢ (↑a)⁻¹.seq n = (↑fun n ↦ (a n)⁻¹).seq n <;>posa:ℕ → ℝn:ℤh:n ≥ 0⊢ (↑a)⁻¹.seq n = (↑fun n ↦ (a n)⁻¹).seq nnega:ℕ → ℝn:ℤh:¬n ≥ 0⊢ (↑a)⁻¹.seq n = (↑fun n ↦ (a n)⁻¹).seq n simp [h]All goals completed! 🐙

Theorem 6.1.19(e) (limit laws). The Sequence.TendsTo version is more usable than the lim version in applications.

theorem declaration uses `sorry`Sequence.tendsTo_inv {a:Sequence} {L:ℝ} (ha: a.TendsTo L) (hnon: L ≠ 0) :
    (a⁻¹).TendsTo (L⁻¹) := bya:SequenceL:ℝha:a.TendsTo Lhnon:L ≠ 0⊢ a⁻¹.TendsTo L⁻¹
  sorryAll goals completed! 🐙

              theorem declaration uses `sorry`Sequence.lim_inv {a:Sequence} (ha: a.Convergent) (hnon: lim a ≠ 0) :
  (a⁻¹).Convergent ∧ lim (a⁻¹) = (lim a)⁻¹ := bya:Sequenceha:a.Convergenthnon:lim a ≠ 0⊢ a⁻¹.Convergent ∧ lim a⁻¹ = (lim a)⁻¹
  sorryAll goals completed! 🐙noncomputable instance Sequence.inst_div : Div Sequence where
  div a b := {
    m := min a.m b.m
    seq n := a n / b n
    vanish n hn := bya:Sequenceb:Sequencen:ℤhn:n < min a.m b.m⊢ a.seq n / b.seq n = 0 simp [a.vanish n (by grind), b.vanish n (by grind)]All goals completed! 🐙
  }@[simp]
theorem Sequence.div_eval {a b: Sequence} (n:ℤ) : (a / b) n = a n / b n := rfltheorem Sequence.div_coe (a b: ℕ → ℝ) : (a:Sequence) / (b:Sequence) = (fun n ↦ a n / b n) := bya:ℕ → ℝb:ℕ → ℝ⊢ ↑a / ↑b = ↑fun n ↦ a n / b n
  ext nma:ℕ → ℝb:ℕ → ℝ⊢ (↑a / ↑b).m = (↑fun n ↦ a n / b n).mseq.ha:ℕ → ℝb:ℕ → ℝn:ℤ⊢ (↑a / ↑b).seq n = (↑fun n ↦ a n / b n).seq n; rflseq.ha:ℕ → ℝb:ℕ → ℝn:ℤ⊢ (↑a / ↑b).seq n = (↑fun n ↦ a n / b n).seq n
  by_cases h:n ≥ 0posa:ℕ → ℝb:ℕ → ℝn:ℤh:n ≥ 0⊢ (↑a / ↑b).seq n = (↑fun n ↦ a n / b n).seq nnega:ℕ → ℝb:ℕ → ℝn:ℤh:¬n ≥ 0⊢ (↑a / ↑b).seq n = (↑fun n ↦ a n / b n).seq n <;>posa:ℕ → ℝb:ℕ → ℝn:ℤh:n ≥ 0⊢ (↑a / ↑b).seq n = (↑fun n ↦ a n / b n).seq nnega:ℕ → ℝb:ℕ → ℝn:ℤh:¬n ≥ 0⊢ (↑a / ↑b).seq n = (↑fun n ↦ a n / b n).seq n simp [h]All goals completed! 🐙

Theorem 6.1.19(f) (limit laws). The Sequence.TendsTo version is more usable than the lim version in applications.

theorem declaration uses `sorry`Sequence.tendsTo_div {a b:Sequence} {L M:ℝ} (ha: a.TendsTo L) (hb: b.TendsTo M) (hnon: M ≠ 0) :
    (a / b).TendsTo (L / M) := bya:Sequenceb:SequenceL:ℝM:ℝha:a.TendsTo Lhb:b.TendsTo Mhnon:M ≠ 0⊢ (a / b).TendsTo (L / M)
  sorryAll goals completed! 🐙

              theorem declaration uses `sorry`Sequence.lim_div {a b:Sequence} (ha: a.Convergent) (hb: b.Convergent) (hnon: lim b ≠ 0) :
  (a / b).Convergent ∧ lim (a / b) = lim a / lim b := bya:Sequenceb:Sequenceha:a.Convergenthb:b.Convergenthnon:lim b ≠ 0⊢ (a / b).Convergent ∧ lim (a / b) = lim a / lim b
  sorryAll goals completed! 🐙instance Sequence.inst_max : Max Sequence where
  max a b := {
    m := min a.m b.m
    seq n := max (a n) (b n)
    vanish n hn := bya:Sequenceb:Sequencen:ℤhn:n < min a.m b.m⊢ max (a.seq n) (b.seq n) = 0 simp [a.vanish n (by grind), b.vanish n (by grind)]All goals completed! 🐙
  }@[simp]
theorem Sequence.max_eval {a b: Sequence} (n:ℤ) : (a ⊔ b) n = (a n) ⊔ (b n) := rfltheorem Sequence.max_coe (a b: ℕ → ℝ) : (a:Sequence) ⊔ (b:Sequence) = (fun n ↦ max (a n) (b n)) := bya:ℕ → ℝb:ℕ → ℝ⊢ ↑a ⊔ ↑b = ↑fun n ↦ max (a n) (b n)
  ext nma:ℕ → ℝb:ℕ → ℝ⊢ (↑a ⊔ ↑b).m = (↑fun n ↦ max (a n) (b n)).mseq.ha:ℕ → ℝb:ℕ → ℝn:ℤ⊢ (↑a ⊔ ↑b).seq n = (↑fun n ↦ max (a n) (b n)).seq n; rflseq.ha:ℕ → ℝb:ℕ → ℝn:ℤ⊢ (↑a ⊔ ↑b).seq n = (↑fun n ↦ max (a n) (b n)).seq n
  by_cases h:n ≥ 0posa:ℕ → ℝb:ℕ → ℝn:ℤh:n ≥ 0⊢ (↑a ⊔ ↑b).seq n = (↑fun n ↦ max (a n) (b n)).seq nnega:ℕ → ℝb:ℕ → ℝn:ℤh:¬n ≥ 0⊢ (↑a ⊔ ↑b).seq n = (↑fun n ↦ max (a n) (b n)).seq n <;>posa:ℕ → ℝb:ℕ → ℝn:ℤh:n ≥ 0⊢ (↑a ⊔ ↑b).seq n = (↑fun n ↦ max (a n) (b n)).seq nnega:ℕ → ℝb:ℕ → ℝn:ℤh:¬n ≥ 0⊢ (↑a ⊔ ↑b).seq n = (↑fun n ↦ max (a n) (b n)).seq n simp [h]All goals completed! 🐙

Theorem 6.1.19(g) (limit laws). The Sequence.TendsTo version is more usable than the lim version in applications.

theorem declaration uses `sorry`Sequence.tendsTo_max {a b:Sequence} {L M:ℝ} (ha: a.TendsTo L) (hb: b.TendsTo M) :
    (max a b).TendsTo (max L M) := bya:Sequenceb:SequenceL:ℝM:ℝha:a.TendsTo Lhb:b.TendsTo M⊢ (a ⊔ b).TendsTo (max L M)
  sorryAll goals completed! 🐙

              theorem declaration uses `sorry`Sequence.lim_max {a b:Sequence} (ha: a.Convergent) (hb: b.Convergent) :
    (max a b).Convergent ∧ lim (max a b) = max (lim a) (lim b) := bya:Sequenceb:Sequenceha:a.Convergenthb:b.Convergent⊢ (a ⊔ b).Convergent ∧ lim (a ⊔ b) = max (lim a) (lim b)
  sorryAll goals completed! 🐙instance Sequence.inst_min : Min Sequence where
  min a b := {
    m := min a.m b.m
    seq n := min (a n) (b n)
    vanish n hn := bya:Sequenceb:Sequencen:ℤhn:n < min a.m b.m⊢ min (a.seq n) (b.seq n) = 0 simp [a.vanish n (by grind), b.vanish n (by grind)]All goals completed! 🐙
  }@[simp]
theorem Sequence.min_eval {a b: Sequence} (n:ℤ) : (a ⊓ b) n = (a n) ⊓ (b n) := rfltheorem Sequence.min_coe (a b: ℕ → ℝ) : (a:Sequence) ⊓ (b:Sequence) = (fun n ↦ min (a n) (b n)) := bya:ℕ → ℝb:ℕ → ℝ⊢ ↑a ⊓ ↑b = ↑fun n ↦ min (a n) (b n)
  ext nma:ℕ → ℝb:ℕ → ℝ⊢ (↑a ⊓ ↑b).m = (↑fun n ↦ min (a n) (b n)).mseq.ha:ℕ → ℝb:ℕ → ℝn:ℤ⊢ (↑a ⊓ ↑b).seq n = (↑fun n ↦ min (a n) (b n)).seq n; rflseq.ha:ℕ → ℝb:ℕ → ℝn:ℤ⊢ (↑a ⊓ ↑b).seq n = (↑fun n ↦ min (a n) (b n)).seq n
  by_cases h:n ≥ 0posa:ℕ → ℝb:ℕ → ℝn:ℤh:n ≥ 0⊢ (↑a ⊓ ↑b).seq n = (↑fun n ↦ min (a n) (b n)).seq nnega:ℕ → ℝb:ℕ → ℝn:ℤh:¬n ≥ 0⊢ (↑a ⊓ ↑b).seq n = (↑fun n ↦ min (a n) (b n)).seq n <;>posa:ℕ → ℝb:ℕ → ℝn:ℤh:n ≥ 0⊢ (↑a ⊓ ↑b).seq n = (↑fun n ↦ min (a n) (b n)).seq nnega:ℕ → ℝb:ℕ → ℝn:ℤh:¬n ≥ 0⊢ (↑a ⊓ ↑b).seq n = (↑fun n ↦ min (a n) (b n)).seq n simp [h]All goals completed! 🐙

Theorem 6.1.19(h) (limit laws)

theorem declaration uses `sorry`Sequence.tendsTo_min {a b:Sequence} {L M:ℝ} (ha: a.TendsTo L) (hb: b.TendsTo M) :
    (min a b).TendsTo (min L M) := bya:Sequenceb:SequenceL:ℝM:ℝha:a.TendsTo Lhb:b.TendsTo M⊢ (a ⊓ b).TendsTo (min L M)
  sorryAll goals completed! 🐙

theorem declaration uses `sorry`Sequence.lim_min {a b:Sequence} (ha: a.Convergent) (hb: b.Convergent) :
    (min a b).Convergent ∧ lim (min a b) = min (lim a) (lim b) := bya:Sequenceb:Sequenceha:a.Convergenthb:b.Convergent⊢ (a ⊓ b).Convergent ∧ lim (a ⊓ b) = min (lim a) (lim b)
  sorryAll goals completed! 🐙

Exercise 6.1.1

theorem declaration uses `sorry`Sequence.mono_if {a: ℕ → ℝ} (ha: ∀ n, a (n+1) > a n) {n m:ℕ} (hnm: m > n) : a m > a n := bya:ℕ → ℝha:∀ (n : ℕ), a (n + 1) > a nn:ℕm:ℕhnm:m > n⊢ a m > a n
  sorryAll goals completed! 🐙

Exercise 6.1.3

theorem declaration uses `sorry`Sequence.tendsTo_of_from {a: Sequence} {c:ℝ} (m:ℤ) :
    a.TendsTo c ↔ (a.from m).TendsTo c := bya:Sequencec:ℝm:ℤ⊢ a.TendsTo c ↔ (a.from m).TendsTo c
  sorryAll goals completed! 🐙

Exercise 6.1.4

theorem declaration uses `sorry`Sequence.tendsTo_of_shift {a: Sequence} {c:ℝ} (k:ℕ) :
    a.TendsTo c ↔ (Sequence.mk' a.m (fun n : {n // n ≥ a.m} ↦ a (n+k))).TendsTo c := bya:Sequencec:ℝk:ℕ⊢ a.TendsTo c ↔ (mk' a.m fun n ↦ a.seq (↑n + ↑k)).TendsTo c
  sorryAll goals completed! 🐙

Exercise 6.1.7

theorem declaration uses `sorry`Sequence.isBounded_of_rat (a: Chapter5.Sequence) :
    a.IsBounded ↔ (a:Sequence).IsBounded := bya:Chapter5.Sequence⊢ a.IsBounded ↔ (↑a).IsBounded
  sorryAll goals completed! 🐙

Exercise 6.1.9

theorem declaration uses `sorry`Sequence.lim_div_fail :
    ∃ a b, a.Convergent
    ∧ b.Convergent
    ∧ lim b = 0
    ∧ ¬ ((a / b).Convergent ∧ lim (a / b) = lim a / lim b) := by⊢ ∃ a b, a.Convergent ∧ b.Convergent ∧ lim b = 0 ∧ ¬((a / b).Convergent ∧ lim (a / b) = lim a / lim b)
  sorryAll goals completed! 🐙

              theorem declaration uses `sorry`Chapter5.Sequence.IsCauchy_iff (a:Chapter5.Sequence) :
    a.IsCauchy ↔ ∀ ε > (0:ℝ), ∃ N ≥ a.n₀, ∀ n ≥ N, ∀ m ≥ N, |a n - a m| ≤ ε := bya:Chapter5.Sequence⊢ a.IsCauchy ↔ ∀ ε > 0, ∃ N ≥ a.n₀, ∀ n ≥ N, ∀ m ≥ N, ↑|a.seq n - a.seq m| ≤ ε
  sorryAll goals completed! 🐙end Chapter6-- additional definitions for exercise 6.1.10
abbrev Real.SeqCloseSeq (ε: ℝ) (a b: Chapter5.Sequence) : Prop :=
  ∀ n, n ≥ a.n₀ → n ≥ b.n₀ → ε.Close (a n) (b n)abbrev Real.SeqEventuallyClose (ε: ℝ) (a b: Chapter5.Sequence): Prop :=
  ∃ N, ε.SeqCloseSeq (a.from N) (b.from N)-- extended definition of rational sequences equivalence but with positive real ε
abbrev Chapter5.Sequence.RatEquiv (a b: ℕ → ℚ) : Prop :=
  ∀ (ε:ℝ), ε > 0 → ε.SeqEventuallyClose (a:Chapter5.Sequence) (b:Chapter5.Sequence)namespace Chapter6

Exercise 6.1.10

theorem declaration uses `sorry`Chapter5.Sequence.equiv_rat (a b: ℕ → ℚ) :
  Chapter5.Sequence.Equiv a b ↔ Chapter5.Sequence.RatEquiv a b := bya:ℕ → ℚb:ℕ → ℚ⊢ Chapter5.Sequence.Equiv a b ↔ Chapter5.Sequence.RatEquiv a b sorryAll goals completed! 🐙

end Chapter6