Analysis I, Section 6.4: Limsup, liminf, and limit points

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:

Lim sup and lim inf of sequences
Limit points of sequences
Comparison and squeeze tests
Completeness of the reals

abbrev Real.Adherent (ε:ℝ) (a:Chapter6.Sequence) (x:ℝ) := ∃ n ≥ a.m, ε.Close (a n) x

abbrev Real.ContinuallyAdherent (ε:ℝ) (a:Chapter6.Sequence) (x:ℝ) :=
  ∀ N ≥ a.m, ε.Adherent (a.from N) x

namespace Chapter6open EReal

abbrev Sequence.LimitPoint (a:Sequence) (x:ℝ) : Prop :=
  ∀ ε > (0:ℝ), ε.ContinuallyAdherent a x

theorem declaration uses 'sorry'Sequence.limit_point_def (a:Sequence) (x:ℝ) :
  a.LimitPoint x ↔ ∀ ε > 0, ∀ N ≥ a.m, ∃ n ≥ N, |a n - x| ≤ ε := bya:Sequencex:ℝ⊢ a.LimitPoint x ↔ ∀ ε > 0, ∀ N ≥ a.m, ∃ n ≥ N, |a.seq n - x| ≤ ε
    unfold LimitPoint Real.ContinuallyAdherent Real.Adherenta:Sequencex:ℝ⊢ (∀ ε > 0, ∀ N ≥ a.m, ∃ n ≥ (a.from N).m, ε.Close ((a.from N).seq n) x) ↔ ∀ ε > 0, ∀ N ≥ a.m, ∃ n ≥ N, |a.seq n - x| ≤ ε
    sorryAll goals completed! 🐙

noncomputable abbrev Example_6_4_3 : Sequence := (fun (n:ℕ) ↦ 1 - (10:ℝ)^(-(n:ℤ)-1))

Example 6.4.3

declaration uses 'sorry'example : (0.1:ℝ).Adherent Example_6_4_3 0.8 := by⊢ Real.Adherent 0.1 Example_6_4_3 0.8 sorryAll goals completed! 🐙

Example 6.4.3

declaration uses 'sorry'example : ¬ (0.1:ℝ).ContinuallyAdherent Example_6_4_3 0.8 := by⊢ ¬Real.ContinuallyAdherent 0.1 Example_6_4_3 0.8 sorryAll goals completed! 🐙

Example 6.4.3

declaration uses 'sorry'example : (0.1:ℝ).ContinuallyAdherent Example_6_4_3 1 := by⊢ Real.ContinuallyAdherent 0.1 Example_6_4_3 1 sorryAll goals completed! 🐙

Example 6.4.3

declaration uses 'sorry'example : Example_6_4_3.LimitPoint 1 := by⊢ Example_6_4_3.LimitPoint 1 sorryAll goals completed! 🐙

noncomputable abbrev Example_6_4_4 : Sequence :=
  (fun (n:ℕ) ↦ (-1:ℝ)^n * (1 + (10:ℝ)^(-(n:ℤ)-1)))

Example 6.4.4

declaration uses 'sorry'example : (0.1:ℝ).Adherent Example_6_4_4 1 := by⊢ Real.Adherent 0.1 Example_6_4_4 1 sorryAll goals completed! 🐙

Example 6.4.4

declaration uses 'sorry'example : (0.1:ℝ).ContinuallyAdherent Example_6_4_4 1 := by⊢ Real.ContinuallyAdherent 0.1 Example_6_4_4 1 sorryAll goals completed! 🐙

Example 6.4.4

declaration uses 'sorry'example : Example_6_4_4.LimitPoint 1 := by⊢ Example_6_4_4.LimitPoint 1 sorryAll goals completed! 🐙

Example 6.4.4

declaration uses 'sorry'example : Example_6_4_4.LimitPoint (-1) := by⊢ Example_6_4_4.LimitPoint (-1) sorryAll goals completed! 🐙

Example 6.4.4

declaration uses 'sorry'example : ¬ Example_6_4_4.LimitPoint 0 := by⊢ ¬Example_6_4_4.LimitPoint 0 sorryAll goals completed! 🐙

Proposition 6.4.5 / Exercise 6.4.1

theorem declaration uses 'sorry'Sequence.limit_point_of_limit {a:Sequence} {x:ℝ} (h: a.TendsTo x) : a.LimitPoint x := bya:Sequencex:ℝh:a.TendsTo x⊢ a.LimitPoint x
  sorryAll goals completed! 🐙

A technical issue uncovered by the formalization: the upper and lower sequences of a real sequence take values in the extended reals rather than the reals, so the definitions need to be adjusted accordingly.

noncomputable abbrev Sequence.upperseq (a:Sequence) : ℤ → EReal := fun N ↦ (a.from N).sup

noncomputable abbrev Sequence.limsup (a:Sequence) : EReal :=
  sInf { x | ∃ N ≥ a.m, x = a.upperseq N }

noncomputable abbrev Sequence.lowerseq (a:Sequence) : ℤ → EReal := fun N ↦ (a.from N).inf

noncomputable abbrev Sequence.liminf (a:Sequence) : EReal :=
  sSup { x | ∃ N ≥ a.m, x = a.lowerseq N }

noncomputable abbrev Example_6_4_7 : Sequence := (fun (n:ℕ) ↦ (-1:ℝ)^n * (1 + (10:ℝ)^(-(n:ℤ)-1)))

declaration uses 'sorry'example (n:ℕ) :
    Example_6_4_7.upperseq n = if Even n then 1 + (10:ℝ)^(-(n:ℤ)-1) else 1 + (10:ℝ)^(-(n:ℤ)-2) := byn:ℕ⊢ Example_6_4_7.upperseq ↑n = ↑(if Even n then 1 + 10 ^ (-↑n - 1) else 1 + 10 ^ (-↑n - 2))
  sorryAll goals completed! 🐙

declaration uses 'sorry'example : Example_6_4_7.limsup = 1 := by⊢ Example_6_4_7.limsup = 1 sorryAll goals completed! 🐙

declaration uses 'sorry'example (n:ℕ) :
    Example_6_4_7.lowerseq n
    = if Even n then -(1 + (10:ℝ)^(-(n:ℤ)-2)) else -(1 + (10:ℝ)^(-(n:ℤ)-1)) := byn:ℕ⊢ Example_6_4_7.lowerseq ↑n = ↑(if Even n then -(1 + 10 ^ (-↑n - 2)) else -(1 + 10 ^ (-↑n - 1)))
  sorryAll goals completed! 🐙

declaration uses 'sorry'example : Example_6_4_7.liminf = -1 := by⊢ Example_6_4_7.liminf = -1 sorryAll goals completed! 🐙

declaration uses 'sorry'example : Example_6_4_7.sup = (1.1:ℝ) := by⊢ Example_6_4_7.sup = ↑1.1 sorryAll goals completed! 🐙

declaration uses 'sorry'example : Example_6_4_7.inf = (-1.01:ℝ) := by⊢ Example_6_4_7.inf = ↑(-1.01) sorryAll goals completed! 🐙

noncomputable abbrev Example_6_4_8 : Sequence := (fun (n:ℕ) ↦ if Even n then (n+1:ℝ) else -(n:ℝ)-1)

declaration uses 'sorry'example (n:ℕ) : Example_6_4_8.upperseq n = ⊤ := byn:ℕ⊢ Example_6_4_8.upperseq ↑n = ⊤ sorryAll goals completed! 🐙

declaration uses 'sorry'example : Example_6_4_8.limsup = ⊤ := by⊢ Example_6_4_8.limsup = ⊤ sorryAll goals completed! 🐙

declaration uses 'sorry'example (n:ℕ) : Example_6_4_8.lowerseq n = ⊥ := byn:ℕ⊢ Example_6_4_8.lowerseq ↑n = ⊥ sorryAll goals completed! 🐙

declaration uses 'sorry'example : Example_6_4_8.liminf = ⊥ := by⊢ Example_6_4_8.liminf = ⊥ sorryAll goals completed! 🐙

noncomputable abbrev Example_6_4_9 : Sequence :=
  (fun (n:ℕ) ↦ if Even n then (n+1:ℝ)⁻¹ else -(n+1:ℝ)⁻¹)

declaration uses 'sorry'example (n:ℕ) : Example_6_4_9.upperseq n = if Even n then (n+1:ℝ)⁻¹ else -(n+2:ℝ)⁻¹ := byn:ℕ⊢ Example_6_4_9.upperseq ↑n = ↑(if Even n then (↑n + 1)⁻¹ else -(↑n + 2)⁻¹) sorryAll goals completed! 🐙

declaration uses 'sorry'example : Example_6_4_9.limsup = 0 := by⊢ Example_6_4_9.limsup = 0 sorryAll goals completed! 🐙

declaration uses 'sorry'example (n:ℕ) : Example_6_4_9.lowerseq n = if Even n then -(n+2:ℝ)⁻¹ else -(n+1:ℝ)⁻¹ := byn:ℕ⊢ Example_6_4_9.lowerseq ↑n = ↑(if Even n then -(↑n + 2)⁻¹ else -(↑n + 1)⁻¹) sorryAll goals completed! 🐙

declaration uses 'sorry'example : Example_6_4_9.liminf = 0 := by⊢ Example_6_4_9.liminf = 0 sorryAll goals completed! 🐙

noncomputable abbrev Example_6_4_10 : Sequence := (fun (n:ℕ) ↦ (n+1:ℝ))

declaration uses 'sorry'example (n:ℕ) : Example_6_4_10.upperseq n = ⊤ := byn:ℕ⊢ Example_6_4_10.upperseq ↑n = ⊤ sorryAll goals completed! 🐙

declaration uses 'sorry'example : Example_6_4_9.limsup = ⊤ := by⊢ Example_6_4_9.limsup = ⊤ sorryAll goals completed! 🐙

declaration uses 'sorry'example (n:ℕ) : Example_6_4_9.lowerseq n = n+1 := byn:ℕ⊢ Example_6_4_9.lowerseq ↑n = ↑n + 1 sorryAll goals completed! 🐙

declaration uses 'sorry'example : Example_6_4_9.liminf = ⊤ := by⊢ Example_6_4_9.liminf = ⊤ sorryAll goals completed! 🐙

Proposition 6.4.12(a)

theorem Sequence.gt_limsup_bounds {a:Sequence} {x:EReal} (h: x > a.limsup) :
    ∃ N ≥ a.m, ∀ n ≥ N, a n < x := bya:Sequencex:ERealh:x > a.limsup⊢ ∃ N ≥ a.m, ∀ n ≥ N, ↑(a.seq n) < x
  -- This proof is written to follow the structure of the original text.
  simp [limsup, sInf_lt_iff] at ha:Sequencex:ERealh:∃ a_1, (∃ N, a.m ≤ N ∧ a_1 = a.upperseq N) ∧ a_1 < x⊢ ∃ N ≥ a.m, ∀ n ≥ N, ↑(a.seq n) < x
  obtain ⟨_, ⟨ N, ⟨ hN, rfl ⟩ ⟩, ha ⟩ := hintro.intro.intro.introa:Sequencex:ERealN:ℤhN:a.m ≤ Nha:a.upperseq N < x⊢ ∃ N ≥ a.m, ∀ n ≥ N, ↑(a.seq n) < x; use Nha:Sequencex:ERealN:ℤhN:a.m ≤ Nha:a.upperseq N < x⊢ N ≥ a.m ∧ ∀ n ≥ N, ↑(a.seq n) < x
  simp [hN, upperseq] at ha ⊢ha:Sequencex:ERealN:ℤhN:a.m ≤ Nha:(a.from N).sup < x⊢ ∀ (n : ℤ), N ≤ n → ↑(a.seq n) < x; intro n _ha:Sequencex:ERealN:ℤhN:a.m ≤ Nha:(a.from N).sup < xn:ℤa✝:N ≤ n⊢ ↑(a.seq n) < x
  have hn' : n ≥ (a.from N).m := bya:Sequencex:ERealh:x > a.limsup⊢ ∃ N ≥ a.m, ∀ n ≥ N, ↑(a.seq n) < x grindAll goals completed! 🐙
  convert lt_of_le_of_lt ((a.from N).le_sup hn') ha using 1h.e'_3a:Sequencex:ERealN:ℤhN:a.m ≤ Nha:(a.from N).sup < xn:ℤa✝:N ≤ nhn':_fvar.53533 ≥ (Chapter6.Sequence.from _fvar.9041 _fvar.45956).m := ?_mvar.53547⊢ ↑(a.seq n) = ↑((a.from N).seq n)
  grindAll goals completed! 🐙

Proposition 6.4.12(a)

theorem declaration uses 'sorry'Sequence.lt_liminf_bounds {a:Sequence} {y:EReal} (h: y < a.liminf) :
    ∃ N ≥ a.m, ∀ n ≥ N, a n > y := bya:Sequencey:ERealh:y < a.liminf⊢ ∃ N ≥ a.m, ∀ n ≥ N, ↑(a.seq n) > y
  sorryAll goals completed! 🐙

Proposition 6.4.12(b)

theorem Sequence.lt_limsup_bounds {a:Sequence} {x:EReal} (h: x < a.limsup) {N:ℤ} (hN: N ≥ a.m) :
    ∃ n ≥ N, a n > x := bya:Sequencex:ERealh:x < a.limsupN:ℤhN:N ≥ a.m⊢ ∃ n ≥ N, ↑(a.seq n) > x
  -- This proof is written to follow the structure of the original text.
  have hx : x < a.upperseq N := bya:Sequencex:ERealh:x < a.limsupN:ℤhN:N ≥ a.m⊢ ∃ n ≥ N, ↑(a.seq n) > x apply lt_of_lt_of_le h (sInf_le _)a:Sequencex:ERealh:x < a.limsupN:ℤhN:N ≥ a.m⊢ a.upperseq N ∈ {x | ∃ N ≥ a.m, x = a.upperseq N}; simpa:Sequencex:ERealh:x < a.limsupN:ℤhN:N ≥ a.m⊢ ∃ N_1, a.m ≤ N_1 ∧ a.upperseq N = a.upperseq N_1; use NAll goals completed! 🐙
  choose n hn hxn _ using exists_between_lt_sup hxa:Sequencex:ERealh:x < a.limsupN:ℤhN:N ≥ a.mhx:_fvar.57731 < Chapter6.Sequence.upperseq _fvar.57730 _fvar.57733 := ?_mvar.57763n:ℤhn:n ≥ (a.from N).mhxn:x < ↑((a.from N).seq n)a✝:↑((a.from N).seq n) ≤ (a.from N).sup⊢ ∃ n ≥ N, ↑(a.seq n) > x
  grindAll goals completed! 🐙

Proposition 6.4.12(b)

theorem declaration uses 'sorry'Sequence.gt_liminf_bounds {a:Sequence} {x:EReal} (h: x > a.liminf) {N:ℤ} (hN: N ≥ a.m) :
    ∃ n ≥ N, a n < x := bya:Sequencex:ERealh:x > a.liminfN:ℤhN:N ≥ a.m⊢ ∃ n ≥ N, ↑(a.seq n) < x
  sorryAll goals completed! 🐙

Proposition 6.4.12(c) / Exercise 6.4.3

theorem declaration uses 'sorry'Sequence.inf_le_liminf (a:Sequence) : a.inf ≤ a.liminf := bya:Sequence⊢ a.inf ≤ a.liminf sorryAll goals completed! 🐙

Proposition 6.4.12(c) / Exercise 6.4.3

theorem declaration uses 'sorry'Sequence.liminf_le_limsup (a:Sequence) : a.liminf ≤ a.limsup := bya:Sequence⊢ a.liminf ≤ a.limsup sorryAll goals completed! 🐙

Proposition 6.4.12(c) / Exercise 6.4.3

theorem declaration uses 'sorry'Sequence.limsup_le_sup (a:Sequence) : a.limsup ≤ a.sup := bya:Sequence⊢ a.limsup ≤ a.sup sorryAll goals completed! 🐙

Proposition 6.4.12(d) / Exercise 6.4.3

theorem declaration uses 'sorry'Sequence.limit_point_between_liminf_limsup {a:Sequence} {c:ℝ} (h: a.LimitPoint c) :
  a.liminf ≤ c ∧ c ≤ a.limsup := bya:Sequencec:ℝh:a.LimitPoint c⊢ a.liminf ≤ ↑c ∧ ↑c ≤ a.limsup
  sorryAll goals completed! 🐙

Proposition 6.4.12(e) / Exercise 6.4.3

theorem declaration uses 'sorry'Sequence.limit_point_of_limsup {a:Sequence} {L_plus:ℝ} (h: a.limsup = L_plus) :
    a.LimitPoint L_plus := bya:SequenceL_plus:ℝh:a.limsup = ↑L_plus⊢ a.LimitPoint L_plus
  sorryAll goals completed! 🐙

Proposition 6.4.12(e) / Exercise 6.4.3

theorem declaration uses 'sorry'Sequence.limit_point_of_liminf {a:Sequence} {L_minus:ℝ} (h: a.liminf = L_minus) :
    a.LimitPoint L_minus := bya:SequenceL_minus:ℝh:a.liminf = ↑L_minus⊢ a.LimitPoint L_minus
  sorryAll goals completed! 🐙

Proposition 6.4.12(f) / Exercise 6.4.3

theorem declaration uses 'sorry'Sequence.tendsTo_iff_eq_limsup_liminf {a:Sequence} (c:ℝ) :
  a.TendsTo c ↔ a.liminf = c ∧ a.limsup = c := bya:Sequencec:ℝ⊢ a.TendsTo c ↔ a.liminf = ↑c ∧ a.limsup = ↑c
  sorryAll goals completed! 🐙

Lemma 6.4.13 (Comparison principle) / Exercise 6.4.4

theorem declaration uses 'sorry'Sequence.sup_mono {a b:Sequence} (hm: a.m = b.m) (hab: ∀ n ≥ a.m, a n ≤ b n) :
    a.sup ≤ b.sup := bya:Sequenceb:Sequencehm:a.m = b.mhab:∀ n ≥ a.m, a.seq n ≤ b.seq n⊢ a.sup ≤ b.sup sorryAll goals completed! 🐙

Lemma 6.4.13 (Comparison principle) / Exercise 6.4.4

theorem declaration uses 'sorry'Sequence.inf_mono {a b:Sequence} (hm: a.m = b.m) (hab: ∀ n ≥ a.m, a n ≤ b n) :
    a.inf ≤ b.inf := bya:Sequenceb:Sequencehm:a.m = b.mhab:∀ n ≥ a.m, a.seq n ≤ b.seq n⊢ a.inf ≤ b.inf sorryAll goals completed! 🐙

Lemma 6.4.13 (Comparison principle) / Exercise 6.4.4

theorem declaration uses 'sorry'Sequence.limsup_mono {a b:Sequence} (hm: a.m = b.m) (hab: ∀ n ≥ a.m, a n ≤ b n) :
    a.limsup ≤ b.limsup := bya:Sequenceb:Sequencehm:a.m = b.mhab:∀ n ≥ a.m, a.seq n ≤ b.seq n⊢ a.limsup ≤ b.limsup sorryAll goals completed! 🐙

Lemma 6.4.13 (Comparison principle) / Exercise 6.4.4

theorem declaration uses 'sorry'Sequence.liminf_mono {a b:Sequence} (hm: a.m = b.m) (hab: ∀ n ≥ a.m, a n ≤ b n) :
    a.liminf ≤ b.liminf := bya:Sequenceb:Sequencehm:a.m = b.mhab:∀ n ≥ a.m, a.seq n ≤ b.seq n⊢ a.liminf ≤ b.liminf sorryAll goals completed! 🐙

Corollary 6.4.14 (Squeeze test) / Exercise 6.4.5

theorem declaration uses 'sorry'Sequence.lim_of_between {a b c:Sequence} {L:ℝ} (hm: b.m = a.m ∧ c.m = a.m)
  (hab: ∀ n ≥ a.m, a n ≤ b n ∧ b n ≤ c n) (ha: a.TendsTo L) (hb: b.TendsTo L) :
    c.TendsTo L := bya:Sequenceb:Sequencec:SequenceL:ℝhm:b.m = a.m ∧ c.m = a.mhab:∀ n ≥ a.m, a.seq n ≤ b.seq n ∧ b.seq n ≤ c.seq nha:a.TendsTo Lhb:b.TendsTo L⊢ c.TendsTo L sorryAll goals completed! 🐙

Example 6.4.15

declaration uses 'sorry'example : ((fun (n:ℕ) ↦ 2/(n+1:ℝ)):Sequence).TendsTo 0 := by⊢ (↑fun n => 2 / (↑n + 1)).TendsTo 0
  sorryAll goals completed! 🐙

Example 6.4.15

declaration uses 'sorry'example : ((fun (n:ℕ) ↦ -2/(n+1:ℝ)):Sequence).TendsTo 0 := by⊢ (↑fun n => -2 / (↑n + 1)).TendsTo 0
  sorryAll goals completed! 🐙

Example 6.4.15

declaration uses 'sorry'example : ((fun (n:ℕ) ↦ (-1)^n/(n+1:ℝ) + 1 / (n+1)^2):Sequence).TendsTo 0 := by⊢ (↑fun n => (-1) ^ n / (↑n + 1) + 1 / (↑n + 1) ^ 2).TendsTo 0
  sorryAll goals completed! 🐙

Example 6.4.15

declaration uses 'sorry'example : ((fun (n:ℕ) ↦ (2:ℝ)^(-(n:ℤ))):Sequence).TendsTo 0 := by⊢ (↑fun n => 2 ^ (-↑n)).TendsTo 0
  sorryAll goals completed! 🐙

abbrev Sequence.abs (a:Sequence) : Sequence where
  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! 🐙

Corollary 6.4.17 (Zero test for sequences) / Exercise 6.4.7

theorem declaration uses 'sorry'Sequence.tendsTo_zero_iff (a:Sequence) :
  a.TendsTo (0:ℝ) ↔ a.abs.TendsTo (0:ℝ) := bya:Sequence⊢ a.TendsTo 0 ↔ a.abs.TendsTo 0
  sorryAll goals completed! 🐙

This helper lemma, implicit in the textbook proofs of Theorem 6.4.18 and Theorem 6.6.8, is made explicit here.

theorem Sequence.finite_limsup_liminf_of_bounded {a:Sequence} (hbound: a.IsBounded) :
    (∃ L_plus:ℝ, a.limsup = L_plus) ∧ (∃ L_minus:ℝ, a.liminf = L_minus) := bya:Sequencehbound:a.IsBounded⊢ (∃ L_plus, a.limsup = ↑L_plus) ∧ ∃ L_minus, a.liminf = ↑L_minus
  choose M hMpos hbound using hbounda:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy M⊢ (∃ L_plus, a.limsup = ↑L_plus) ∧ ∃ L_minus, a.liminf = ↑L_minus
  have hlimsup_bound : a.limsup ≤ M := bya:Sequencehbound:a.IsBounded⊢ (∃ L_plus, a.limsup = ↑L_plus) ∧ ∃ L_minus, a.liminf = ↑L_minus
    apply a.limsup_le_sup.trans (sup_le_upper _)a:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy M⊢ ∀ n ≥ a.m, ↑(a.seq n) ≤ ↑M
    intro n hNa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mn:ℤhN:n ≥ a.m⊢ ↑(a.seq n) ≤ ↑M; simpa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mn:ℤhN:n ≥ a.m⊢ a.seq n ≤ M
    exact (le_abs_self _).trans (hbound n)All goals completed! 🐙
  have hliminf_bound : -M ≤ a.liminf := bya:Sequencehbound:a.IsBounded⊢ (∃ L_plus, a.limsup = ↑L_plus) ∧ ∃ L_minus, a.liminf = ↑L_minus
    apply (inf_ge_lower _).trans a.inf_le_liminfa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:Chapter6.Sequence.limsup _fvar.100622 ≤ ↑_fvar.100626 := ?_mvar.100807⊢ ∀ n ≥ a.m, ↑(a.seq n) ≥ -↑M
    intro n hNa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:Chapter6.Sequence.limsup _fvar.100622 ≤ ↑_fvar.100626 := ?_mvar.100807n:ℤhN:n ≥ a.m⊢ ↑(a.seq n) ≥ -↑M; simp [←coe_neg]a:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:Chapter6.Sequence.limsup _fvar.100622 ≤ ↑_fvar.100626 := ?_mvar.100807n:ℤhN:n ≥ a.m⊢ -M ≤ a.seq n; rw [neg_le]a:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:Chapter6.Sequence.limsup _fvar.100622 ≤ ↑_fvar.100626 := ?_mvar.100807n:ℤhN:n ≥ a.m⊢ -a.seq n ≤ M
    exact (neg_le_abs _).trans (hbound n)All goals completed! 🐙
  split_andsrefine_1a:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:Chapter6.Sequence.limsup _fvar.100622 ≤ ↑_fvar.100626 := ?_mvar.100807hliminf_bound:-↑_fvar.100626 ≤ Chapter6.Sequence.liminf _fvar.100622 := ?_mvar.102734⊢ ∃ L_plus, a.limsup = ↑L_plusrefine_2a:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:Chapter6.Sequence.limsup _fvar.100622 ≤ ↑_fvar.100626 := ?_mvar.100807hliminf_bound:-↑_fvar.100626 ≤ Chapter6.Sequence.liminf _fvar.100622 := ?_mvar.102734⊢ ∃ L_minus, a.liminf = ↑L_minus
  .refine_1a:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:Chapter6.Sequence.limsup _fvar.100622 ≤ ↑_fvar.100626 := ?_mvar.100807hliminf_bound:-↑_fvar.100626 ≤ Chapter6.Sequence.liminf _fvar.100622 := ?_mvar.102734⊢ ∃ L_plus, a.limsup = ↑L_plus use a.limsup.toRealha:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:Chapter6.Sequence.limsup _fvar.100622 ≤ ↑_fvar.100626 := ?_mvar.100807hliminf_bound:-↑_fvar.100626 ≤ Chapter6.Sequence.liminf _fvar.100622 := ?_mvar.102734⊢ a.limsup = ↑a.limsup.toReal
    symmha:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:Chapter6.Sequence.limsup _fvar.100622 ≤ ↑_fvar.100626 := ?_mvar.100807hliminf_bound:-↑_fvar.100626 ≤ Chapter6.Sequence.liminf _fvar.100622 := ?_mvar.102734⊢ ↑a.limsup.toReal = a.limsup; apply coe_toRealh.hxa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:Chapter6.Sequence.limsup _fvar.100622 ≤ ↑_fvar.100626 := ?_mvar.100807hliminf_bound:-↑_fvar.100626 ≤ Chapter6.Sequence.liminf _fvar.100622 := ?_mvar.102734⊢ a.limsup ≠ ⊤h.h'xa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:Chapter6.Sequence.limsup _fvar.100622 ≤ ↑_fvar.100626 := ?_mvar.100807hliminf_bound:-↑_fvar.100626 ≤ Chapter6.Sequence.liminf _fvar.100622 := ?_mvar.102734⊢ a.limsup ≠ ⊥
    .h.hxa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:Chapter6.Sequence.limsup _fvar.100622 ≤ ↑_fvar.100626 := ?_mvar.100807hliminf_bound:-↑_fvar.100626 ≤ Chapter6.Sequence.liminf _fvar.100622 := ?_mvar.102734⊢ a.limsup ≠ ⊤ contrapose! hlimsup_boundh.hxa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhliminf_bound:-↑_fvar.100626 ≤ Chapter6.Sequence.liminf _fvar.100622 := ?_mvar.102734hlimsup_bound:a.limsup = ⊤⊢ ↑M < a.limsup; simp [hlimsup_bound]All goals completed! 🐙
    replace hliminf_bound := hliminf_bound.trans a.liminf_le_limsuph.h'xa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:Chapter6.Sequence.limsup _fvar.100622 ≤ ↑_fvar.100626 := ?_mvar.100807hliminf_bound:?_mvar.121956 := LE.le.trans _fvar.102735 (Chapter6.Sequence.liminf_le_limsup _fvar.100622)⊢ a.limsup ≠ ⊥
    contrapose! hliminf_boundh.h'xa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:Chapter6.Sequence.limsup _fvar.100622 ≤ ↑_fvar.100626 := ?_mvar.100807hliminf_bound:a.limsup = ⊥⊢ a.limsup < -↑M; simp [hliminf_bound, ←coe_neg]All goals completed! 🐙
  use a.liminf.toRealha:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:Chapter6.Sequence.limsup _fvar.100622 ≤ ↑_fvar.100626 := ?_mvar.100807hliminf_bound:-↑_fvar.100626 ≤ Chapter6.Sequence.liminf _fvar.100622 := ?_mvar.102734⊢ a.liminf = ↑a.liminf.toReal; symmha:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:Chapter6.Sequence.limsup _fvar.100622 ≤ ↑_fvar.100626 := ?_mvar.100807hliminf_bound:-↑_fvar.100626 ≤ Chapter6.Sequence.liminf _fvar.100622 := ?_mvar.102734⊢ ↑a.liminf.toReal = a.liminf; apply coe_toRealh.hxa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:Chapter6.Sequence.limsup _fvar.100622 ≤ ↑_fvar.100626 := ?_mvar.100807hliminf_bound:-↑_fvar.100626 ≤ Chapter6.Sequence.liminf _fvar.100622 := ?_mvar.102734⊢ a.liminf ≠ ⊤h.h'xa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:Chapter6.Sequence.limsup _fvar.100622 ≤ ↑_fvar.100626 := ?_mvar.100807hliminf_bound:-↑_fvar.100626 ≤ Chapter6.Sequence.liminf _fvar.100622 := ?_mvar.102734⊢ a.liminf ≠ ⊥
  .h.hxa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:Chapter6.Sequence.limsup _fvar.100622 ≤ ↑_fvar.100626 := ?_mvar.100807hliminf_bound:-↑_fvar.100626 ≤ Chapter6.Sequence.liminf _fvar.100622 := ?_mvar.102734⊢ a.liminf ≠ ⊤ apply a.liminf_le_limsup.trans at hlimsup_boundh.hxa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhliminf_bound:-↑_fvar.100626 ≤ Chapter6.Sequence.liminf _fvar.100622 := ?_mvar.102734hlimsup_bound:a.liminf ≤ ↑M⊢ a.liminf ≠ ⊤
    contrapose! hlimsup_boundh.hxa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhliminf_bound:-↑_fvar.100626 ≤ Chapter6.Sequence.liminf _fvar.100622 := ?_mvar.102734hlimsup_bound:a.liminf = ⊤⊢ ↑M < a.liminf; simp [hlimsup_bound]All goals completed! 🐙
  contrapose! hliminf_boundh.h'xa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:Chapter6.Sequence.limsup _fvar.100622 ≤ ↑_fvar.100626 := ?_mvar.100807hliminf_bound:a.liminf = ⊥⊢ a.liminf < -↑M; simp [hliminf_bound, ←coe_neg]All goals completed! 🐙

Theorem 6.4.18 (Completeness of the reals)

theorem Sequence.Cauchy_iff_convergent (a:Sequence) :
  a.IsCauchy ↔ a.Convergent := bya:Sequence⊢ a.IsCauchy ↔ a.Convergent
  -- This proof is written to follow the structure of the original text.
  refine ⟨ ?_, IsCauchy.convergent ⟩a:Sequence⊢ a.IsCauchy → a.Convergent; intro ha:Sequenceh:a.IsCauchy⊢ a.Convergent
  have ⟨ ⟨ L_plus, hL_plus ⟩, ⟨ L_minus, hL_minus ⟩ ⟩ :=
    finite_limsup_liminf_of_bounded (bounded_of_cauchy h)a:Sequenceh:a.IsCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minus⊢ a.Convergent
  use L_minusha:Sequenceh:a.IsCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minus⊢ a.TendsTo L_minus; simp [tendsTo_iff_eq_limsup_liminf, hL_minus, hL_plus]ha:Sequenceh:a.IsCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minus⊢ L_plus = L_minus
  have hlow : 0 ≤ L_plus - L_minus := bya:Sequence⊢ a.IsCauchy ↔ a.Convergent
    have := a.liminf_le_limsupa:Sequenceh:a.IsCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minusthis:?_mvar.208155 := Chapter6.Sequence.liminf_le_limsup _fvar.174394⊢ 0 ≤ L_plus - L_minus; simp [hL_minus, hL_plus] at thisa:Sequenceh:a.IsCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minusthis:L_minus ≤ L_plus⊢ 0 ≤ L_plus - L_minus; grindAll goals completed! 🐙
  have hup (ε:ℝ) (hε: ε>0) : L_plus - L_minus ≤ 2*ε := bya:Sequence⊢ a.IsCauchy ↔ a.Convergent
    specialize h ε hεa:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ _fvar.174481 - _fvar.174483 := ?_mvar.208149ε:ℝhε:ε > 0h:ε.EventuallySteady a⊢ L_plus - L_minus ≤ 2 * ε; choose N hN hsteady using ha:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ _fvar.174481 - _fvar.174483 := ?_mvar.208149ε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:ε.Steady (a.from N)⊢ L_plus - L_minus ≤ 2 * ε
    have hN0 : N ≥ (a.from N).m := bya:Sequence⊢ a.IsCauchy ↔ a.Convergent grindAll goals completed! 🐙
    have hN1 : (a.from N).seq N = a.seq N := bya:Sequence⊢ a.IsCauchy ↔ a.Convergent grindAll goals completed! 🐙
    have h1 : (a N - ε:ℝ) ≤ (a.from N).inf := bya:Sequence⊢ a.IsCauchy ↔ a.Convergent
      apply inf_ge_lowerha:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ _fvar.174481 - _fvar.174483 := ?_mvar.208149ε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:ε.Steady (a.from N)hN0:_fvar.245474 ≥ (Chapter6.Sequence.from _fvar.174394 _fvar.245474).m := ?_mvar.245502hN1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.249329⊢ ∀ n ≥ (a.from N).m, ↑((a.from N).seq n) ≥ ↑(a.seq N - ε); grind [Real.dist_eq, abs_le',EReal.coe_le_coe_iff]All goals completed! 🐙
    have h2 : (a.from N).inf ≤ L_minus := bya:Sequence⊢ a.IsCauchy ↔ a.Convergent
      simp_rw [←hL_minus, liminf, lowerseq]a:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ _fvar.174481 - _fvar.174483 := ?_mvar.208149ε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:ε.Steady (a.from N)hN0:_fvar.245474 ≥ (Chapter6.Sequence.from _fvar.174394 _fvar.245474).m := ?_mvar.245502hN1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.249329h1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.254083⊢ (a.from N).inf ≤ sSup {x | ∃ N ≥ a.m, x = (a.from N).inf}; apply le_sSupa._@.Mathlib.Order.CompleteLattice.Defs._hyg.240a:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ _fvar.174481 - _fvar.174483 := ?_mvar.208149ε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:ε.Steady (a.from N)hN0:_fvar.245474 ≥ (Chapter6.Sequence.from _fvar.174394 _fvar.245474).m := ?_mvar.245502hN1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.249329h1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.254083⊢ (a.from N).inf ∈ {x | ∃ N ≥ a.m, x = (a.from N).inf}; simpa._@.Mathlib.Order.CompleteLattice.Defs._hyg.240a:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ _fvar.174481 - _fvar.174483 := ?_mvar.208149ε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:ε.Steady (a.from N)hN0:_fvar.245474 ≥ (Chapter6.Sequence.from _fvar.174394 _fvar.245474).m := ?_mvar.245502hN1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.249329h1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.254083⊢ ∃ N_1, a.m ≤ N_1 ∧ (a.from N).inf = (a.from N_1).inf; use NAll goals completed! 🐙
    have h3 : (a.from N).sup ≤ (a N + ε:ℝ) := bya:Sequence⊢ a.IsCauchy ↔ a.Convergent
      apply sup_le_upperha:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ _fvar.174481 - _fvar.174483 := ?_mvar.208149ε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:ε.Steady (a.from N)hN0:_fvar.245474 ≥ (Chapter6.Sequence.from _fvar.174394 _fvar.245474).m := ?_mvar.245502hN1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.249329h1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.254083h2:(Chapter6.Sequence.from _fvar.174394 _fvar.245474).inf ≤ ↑_fvar.174483 := ?_mvar.259178⊢ ∀ n ≥ (a.from N).m, ↑((a.from N).seq n) ≤ ↑(a.seq N + ε); grind [EReal.coe_le_coe_iff, Real.dist_eq, abs_le']All goals completed! 🐙
    have h4 : L_plus ≤ (a.from N).sup := bya:Sequence⊢ a.IsCauchy ↔ a.Convergent
      simp_rw [←hL_plus, limsup, upperseq]a:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ _fvar.174481 - _fvar.174483 := ?_mvar.208149ε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:ε.Steady (a.from N)hN0:_fvar.245474 ≥ (Chapter6.Sequence.from _fvar.174394 _fvar.245474).m := ?_mvar.245502hN1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.249329h1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.254083h2:(Chapter6.Sequence.from _fvar.174394 _fvar.245474).inf ≤ ↑_fvar.174483 := ?_mvar.259178h3:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.294570⊢ sInf {x | ∃ N ≥ a.m, x = (a.from N).sup} ≤ (a.from N).sup; apply sInf_lea._@.Mathlib.Order.CompleteLattice.Defs._hyg.754a:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ _fvar.174481 - _fvar.174483 := ?_mvar.208149ε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:ε.Steady (a.from N)hN0:_fvar.245474 ≥ (Chapter6.Sequence.from _fvar.174394 _fvar.245474).m := ?_mvar.245502hN1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.249329h1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.254083h2:(Chapter6.Sequence.from _fvar.174394 _fvar.245474).inf ≤ ↑_fvar.174483 := ?_mvar.259178h3:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.294570⊢ (a.from N).sup ∈ {x | ∃ N ≥ a.m, x = (a.from N).sup}; simpa._@.Mathlib.Order.CompleteLattice.Defs._hyg.754a:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ _fvar.174481 - _fvar.174483 := ?_mvar.208149ε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:ε.Steady (a.from N)hN0:_fvar.245474 ≥ (Chapter6.Sequence.from _fvar.174394 _fvar.245474).m := ?_mvar.245502hN1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.249329h1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.254083h2:(Chapter6.Sequence.from _fvar.174394 _fvar.245474).inf ≤ ↑_fvar.174483 := ?_mvar.259178h3:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.294570⊢ ∃ N_1, a.m ≤ N_1 ∧ (a.from N).sup = (a.from N_1).sup; use NAll goals completed! 🐙
    replace h1 := h1.trans h2a:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ _fvar.174481 - _fvar.174483 := ?_mvar.208149ε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:ε.Steady (a.from N)hN0:_fvar.245474 ≥ (Chapter6.Sequence.from _fvar.174394 _fvar.245474).m := ?_mvar.245502hN1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.249329h2:(Chapter6.Sequence.from _fvar.174394 _fvar.245474).inf ≤ ↑_fvar.174483 := ?_mvar.259178h3:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.294570h4:↑_fvar.174481 ≤ (Chapter6.Sequence.from _fvar.174394 _fvar.245474).sup := ?_mvar.300668h1:?_mvar.335983 := LE.le.trans _fvar.254084 _fvar.259179⊢ L_plus - L_minus ≤ 2 * ε
    replace h4 := h4.trans h3a:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ _fvar.174481 - _fvar.174483 := ?_mvar.208149ε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:ε.Steady (a.from N)hN0:_fvar.245474 ≥ (Chapter6.Sequence.from _fvar.174394 _fvar.245474).m := ?_mvar.245502hN1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.249329h2:(Chapter6.Sequence.from _fvar.174394 _fvar.245474).inf ≤ ↑_fvar.174483 := ?_mvar.259178h3:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.294570h1:?_mvar.335983 := LE.le.trans _fvar.254084 _fvar.259179h4:?_mvar.336027 := LE.le.trans _fvar.300669 _fvar.294571⊢ L_plus - L_minus ≤ 2 * ε
    grind [EReal.coe_le_coe_iff]All goals completed! 🐙
  obtain hlow | hlow := le_iff_lt_or_eq.mp hlowh.inla:Sequenceh:a.IsCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow✝:0 ≤ _fvar.174481 - _fvar.174483 := ?_mvar.208149hup:∀ ε > 0, _fvar.174481 - _fvar.174483 ≤ 2 * ε := fun ε hε => @?_mvar.245455 ε hεhlow:0 < L_plus - L_minus⊢ L_plus = L_minush.inra:Sequenceh:a.IsCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow✝:0 ≤ _fvar.174481 - _fvar.174483 := ?_mvar.208149hup:∀ ε > 0, _fvar.174481 - _fvar.174483 ≤ 2 * ε := fun ε hε => @?_mvar.245455 ε hεhlow:0 = L_plus - L_minus⊢ L_plus = L_minus
  .h.inla:Sequenceh:a.IsCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow✝:0 ≤ _fvar.174481 - _fvar.174483 := ?_mvar.208149hup:∀ ε > 0, _fvar.174481 - _fvar.174483 ≤ 2 * ε := fun ε hε => @?_mvar.245455 ε hεhlow:0 < L_plus - L_minus⊢ L_plus = L_minus specialize hup ((L_plus - L_minus)/3) ?_h.inla:Sequenceh:a.IsCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow✝:0 ≤ _fvar.174481 - _fvar.174483 := ?_mvar.208149hup:∀ ε > 0, _fvar.174481 - _fvar.174483 ≤ 2 * ε := fun ε hε => @?_mvar.245455 ε hεhlow:0 < L_plus - L_minus⊢ (L_plus - L_minus) / 3 > 0h.inla:Sequenceh:a.IsCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow✝:0 ≤ _fvar.174481 - _fvar.174483 := ?_mvar.208149hlow:0 < L_plus - L_minushup:L_plus - L_minus ≤ 2 * ((L_plus - L_minus) / 3)⊢ L_plus = L_minus <;>h.inla:Sequenceh:a.IsCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow✝:0 ≤ _fvar.174481 - _fvar.174483 := ?_mvar.208149hup:∀ ε > 0, _fvar.174481 - _fvar.174483 ≤ 2 * ε := fun ε hε => @?_mvar.245455 ε hεhlow:0 < L_plus - L_minus⊢ (L_plus - L_minus) / 3 > 0h.inla:Sequenceh:a.IsCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow✝:0 ≤ _fvar.174481 - _fvar.174483 := ?_mvar.208149hlow:0 < L_plus - L_minushup:L_plus - L_minus ≤ 2 * ((L_plus - L_minus) / 3)⊢ L_plus = L_minus linarithAll goals completed! 🐙
  grindAll goals completed! 🐙

Exercise 6.4.6

theorem declaration uses 'sorry'Sequence.sup_not_strict_mono : ∃ (a b:ℕ → ℝ), (∀ n, a n < b n) ∧ (a:Sequence).sup ≠ (b:Sequence).sup := by⊢ ∃ a b, (∀ (n : ℕ), a n < b n) ∧ (↑a).sup ≠ (↑b).sup
  sorryAll goals completed! 🐙

/- Exercise 6.4.7 -/
def declaration uses 'sorry'Sequence.tendsTo_real_iff :
  Decidable (∀ (a:Sequence) (x:ℝ), a.TendsTo x ↔ a.abs.TendsTo x) := by⊢ Decidable (∀ (a : Sequence) (x : ℝ), a.TendsTo x ↔ a.abs.TendsTo x)
  -- The first line of this construction should be `apply isTrue` or `apply isFalse`.
  sorryAll goals completed! 🐙

This definition is needed for Exercises 6.4.8 and 6.4.9.

abbrev Sequence.ExtendedLimitPoint (a:Sequence) (x:EReal) : Prop := if x = ⊤ then ¬ a.BddAbove else if x = ⊥ then ¬ a.BddBelow else a.LimitPoint x.toReal

Exercise 6.4.8

theorem declaration uses 'sorry'Sequence.extended_limit_point_of_limsup (a:Sequence) : a.ExtendedLimitPoint a.limsup := bya:Sequence⊢ a.ExtendedLimitPoint a.limsup sorryAll goals completed! 🐙

Exercise 6.4.8

theorem declaration uses 'sorry'Sequence.extended_limit_point_of_liminf (a:Sequence) : a.ExtendedLimitPoint a.liminf := bya:Sequence⊢ a.ExtendedLimitPoint a.liminf sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Sequence.extended_limit_point_le_limsup {a:Sequence} {L:EReal} (h:a.ExtendedLimitPoint L): L ≤ a.limsup := bya:SequenceL:ERealh:a.ExtendedLimitPoint L⊢ L ≤ a.limsup sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Sequence.extended_limit_point_ge_liminf {a:Sequence} {L:EReal} (h:a.ExtendedLimitPoint L): L ≥ a.liminf := bya:SequenceL:ERealh:a.ExtendedLimitPoint L⊢ L ≥ a.liminf sorryAll goals completed! 🐙

Exercise 6.4.9

theorem declaration uses 'sorry'Sequence.exists_three_limit_points : ∃ a:Sequence, ∀ L:EReal, a.ExtendedLimitPoint L ↔ L = ⊥ ∨ L = 0 ∨ L = ⊤ := by⊢ ∃ a, ∀ (L : EReal), a.ExtendedLimitPoint L ↔ L = ⊥ ∨ L = 0 ∨ L = ⊤ sorryAll goals completed! 🐙

Exercise 6.4.10

theorem declaration uses 'sorry'Sequence.limit_points_of_limit_points {a b:Sequence} {c:ℝ} (hab: ∀ n ≥ b.m, a.LimitPoint (b n)) (hbc: b.LimitPoint c) : a.LimitPoint c := bya:Sequenceb:Sequencec:ℝhab:∀ n ≥ b.m, a.LimitPoint (b.seq n)hbc:b.LimitPoint c⊢ a.LimitPoint c sorryAll goals completed! 🐙

end Chapter6