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

@[reducible, inline]

abbrev Real.Adherent (ε : ℝ) (a : Chapter6.Sequence) (x : ℝ) : Prop

Equations

• ε.Adherent a x = ∃ n ≥ a.m, ε.Close (a.seq n) x

@[reducible, inline]

abbrev Real.ContinuallyAdherent (ε : ℝ) (a : Chapter6.Sequence) (x : ℝ) : Prop

Equations

• ε.ContinuallyAdherent a x = ∀ N ≥ a.m, ε.Adherent (a.from N) x

@[reducible, inline]

abbrev Chapter6.Sequence.LimitPoint (a : Sequence) (x : ℝ) : Prop

Equations

• a.LimitPoint x = ∀ ε > 0, ε.ContinuallyAdherent a x

theorem Chapter6.Sequence.limit_point_def (a : Sequence) (x : ℝ) : a.LimitPoint x ↔ ∀ ε > 0, ∀ N ≥ a.m, ∃ n ≥ N, |a.seq n - x| ≤ ε

@[reducible, inline]

noncomputable abbrev Chapter6.Example_6_4_3 : Sequence

Equations

• Chapter6.Example_6_4_3 = ↑fun (n : ℕ) => 1 - 10 ^ (-↑n - 1)

@[reducible, inline]

noncomputable abbrev Chapter6.Example_6_4_4 : Sequence

Equations

• Chapter6.Example_6_4_4 = ↑fun (n : ℕ) => (-1) ^ n * (1 + 10 ^ (-↑n - 1))

theorem Chapter6.Sequence.limit_point_of_limit {a : Sequence} {x : ℝ} (h : a.TendsTo x) : a.LimitPoint x

Proposition 6.4.5 / Exercise 6.4.1

@[reducible, inline]

noncomputable abbrev Chapter6.Sequence.upperseq (a : Sequence) : ℤ → EReal

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.

Equations

• a.upperseq N = (a.from N).sup

@[reducible, inline]

noncomputable abbrev Chapter6.Sequence.limsup (a : Sequence) : EReal

Equations

• a.limsup = sInf {x : EReal | ∃ N ≥ a.m, x = a.upperseq N}

@[reducible, inline]

noncomputable abbrev Chapter6.Sequence.lowerseq (a : Sequence) : ℤ → EReal

Equations

• a.lowerseq N = (a.from N).inf

@[reducible, inline]

noncomputable abbrev Chapter6.Sequence.liminf (a : Sequence) : EReal

Equations

• a.liminf = sSup {x : EReal | ∃ N ≥ a.m, x = a.lowerseq N}

@[reducible, inline]

noncomputable abbrev Chapter6.Example_6_4_7 : Sequence

Equations

• Chapter6.Example_6_4_7 = ↑fun (n : ℕ) => (-1) ^ n * (1 + 10 ^ (-↑n - 1))

@[reducible, inline]

noncomputable abbrev Chapter6.Example_6_4_8 : Sequence

Equations

• Chapter6.Example_6_4_8 = ↑fun (n : ℕ) => if Even n then ↑n + 1 else -↑n - 1

@[reducible, inline]

noncomputable abbrev Chapter6.Example_6_4_9 : Sequence

Equations

• Chapter6.Example_6_4_9 = ↑fun (n : ℕ) => if Even n then (↑n + 1)⁻¹ else -(↑n + 1)⁻¹

@[reducible, inline]

noncomputable abbrev Chapter6.Example_6_4_10 : Sequence

Equations

• Chapter6.Example_6_4_10 = ↑fun (n : ℕ) => ↑n + 1

theorem Chapter6.Sequence.gt_limsup_bounds {a : Sequence} {x : EReal} (h : x > a.limsup) : ∃ N ≥ a.m, ∀ n ≥ N, ↑(a.seq n) < x

Proposition 6.4.12(a)

theorem Chapter6.Sequence.lt_liminf_bounds {a : Sequence} {y : EReal} (h : y < a.liminf) : ∃ N ≥ a.m, ∀ n ≥ N, ↑(a.seq n) > y

Proposition 6.4.12(a)

theorem Chapter6.Sequence.lt_limsup_bounds {a : Sequence} {x : EReal} (h : x < a.limsup) {N : ℤ} (hN : N ≥ a.m) : ∃ n ≥ N, ↑(a.seq n) > x

Proposition 6.4.12(b)

theorem Chapter6.Sequence.gt_liminf_bounds {a : Sequence} {x : EReal} (h : x > a.liminf) {N : ℤ} (hN : N ≥ a.m) : ∃ n ≥ N, ↑(a.seq n) < x

Proposition 6.4.12(b)

theorem Chapter6.Sequence.inf_le_liminf (a : Sequence) : a.inf ≤ a.liminf

Proposition 6.4.12(c) / Exercise 6.4.3

theorem Chapter6.Sequence.liminf_le_limsup (a : Sequence) : a.liminf ≤ a.limsup

Proposition 6.4.12(c) / Exercise 6.4.3

theorem Chapter6.Sequence.limsup_le_sup (a : Sequence) : a.limsup ≤ a.sup

Proposition 6.4.12(c) / Exercise 6.4.3

theorem Chapter6.Sequence.limit_point_between_liminf_limsup {a : Sequence} {c : ℝ} (h : a.LimitPoint c) : a.liminf ≤ ↑c ∧ ↑c ≤ a.limsup

Proposition 6.4.12(d) / Exercise 6.4.3

theorem Chapter6.Sequence.limit_point_of_limsup {a : Sequence} {L_plus : ℝ} (h : a.limsup = ↑L_plus) : a.LimitPoint L_plus

Proposition 6.4.12(e) / Exercise 6.4.3

theorem Chapter6.Sequence.limit_point_of_liminf {a : Sequence} {L_minus : ℝ} (h : a.liminf = ↑L_minus) : a.LimitPoint L_minus

Proposition 6.4.12(e) / Exercise 6.4.3

theorem Chapter6.Sequence.tendsTo_iff_eq_limsup_liminf {a : Sequence} (c : ℝ) : a.TendsTo c ↔ a.liminf = ↑c ∧ a.limsup = ↑c

Proposition 6.4.12(f) / Exercise 6.4.3

theorem Chapter6.Sequence.sup_mono {a b : Sequence} (hm : a.m = b.m) (hab : ∀ n ≥ a.m, a.seq n ≤ b.seq n) : a.sup ≤ b.sup

Lemma 6.4.13 (Comparison principle) / Exercise 6.4.4

theorem Chapter6.Sequence.inf_mono {a b : Sequence} (hm : a.m = b.m) (hab : ∀ n ≥ a.m, a.seq n ≤ b.seq n) : a.inf ≤ b.inf

Lemma 6.4.13 (Comparison principle) / Exercise 6.4.4

theorem Chapter6.Sequence.limsup_mono {a b : Sequence} (hm : a.m = b.m) (hab : ∀ n ≥ a.m, a.seq n ≤ b.seq n) : a.limsup ≤ b.limsup

Lemma 6.4.13 (Comparison principle) / Exercise 6.4.4

theorem Chapter6.Sequence.liminf_mono {a b : Sequence} (hm : a.m = b.m) (hab : ∀ n ≥ a.m, a.seq n ≤ b.seq n) : a.liminf ≤ b.liminf

Lemma 6.4.13 (Comparison principle) / Exercise 6.4.4

theorem Chapter6.Sequence.lim_of_between {a b c : Sequence} {L : ℝ} (hm : b.m = a.m ∧ c.m = a.m) (hab : ∀ n ≥ a.m, a.seq n ≤ b.seq n ∧ b.seq n ≤ c.seq n) (ha : a.TendsTo L) (hb : b.TendsTo L) : c.TendsTo L

Corollary 6.4.14 (Squeeze test) / Exercise 6.4.5

@[reducible, inline]

abbrev Chapter6.Sequence.abs (a : Sequence) : Sequence

Equations

• a.abs = { m := a.m, seq := fun (n : ℤ) => |a.seq n|, vanish := ⋯ }

theorem Chapter6.Sequence.tendsTo_zero_iff (a : Sequence) : a.TendsTo 0 ↔ a.abs.TendsTo 0

Corollary 6.4.17 (Zero test for sequences) / Exercise 6.4.7

theorem Chapter6.Sequence.finite_limsup_liminf_of_bounded {a : Sequence} (hbound : a.IsBounded) : (∃ (L_plus : ℝ), a.limsup = ↑L_plus) ∧ ∃ (L_minus : ℝ), a.liminf = ↑L_minus

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

theorem Chapter6.Sequence.Cauchy_iff_convergent (a : Sequence) : a.IsCauchy ↔ a.Convergent

Theorem 6.4.18 (Completeness of the reals)

theorem Chapter6.Sequence.sup_not_strict_mono : ∃ (a : ℕ → ℝ) (b : ℕ → ℝ), (∀ (n : ℕ), a n < b n) ∧ (↑a).sup ≠ (↑b).sup

Exercise 6.4.6

def Chapter6.Sequence.tendsTo_real_iff : Decidable (∀ (a : Sequence) (x : ℝ), a.TendsTo x ↔ a.abs.TendsTo x)

Equations

• Chapter6.Sequence.tendsTo_real_iff = sorry

@[reducible, inline]

abbrev Chapter6.Sequence.ExtendedLimitPoint (a : Sequence) (x : EReal) : Prop

This definition is needed for Exercises 6.4.8 and 6.4.9.

Equations

• a.ExtendedLimitPoint x = if x = ⊤ then ¬a.BddAbove else if x = ⊥ then ¬a.BddBelow else a.LimitPoint x.toReal

theorem Chapter6.Sequence.extended_limit_point_of_limsup (a : Sequence) : a.ExtendedLimitPoint a.limsup

Exercise 6.4.8

theorem Chapter6.Sequence.extended_limit_point_of_liminf (a : Sequence) : a.ExtendedLimitPoint a.liminf

Exercise 6.4.8

theorem Chapter6.Sequence.extended_limit_point_le_limsup {a : Sequence} {L : EReal} (h : a.ExtendedLimitPoint L) : L ≤ a.limsup

theorem Chapter6.Sequence.extended_limit_point_ge_liminf {a : Sequence} {L : EReal} (h : a.ExtendedLimitPoint L) : L ≥ a.liminf

theorem Chapter6.Sequence.exists_three_limit_points : ∃ (a : Sequence), ∀ (L : EReal), a.ExtendedLimitPoint L ↔ L = ⊥ ∨ L = 0 ∨ L = ⊤

Exercise 6.4.9

theorem Chapter6.Sequence.limit_points_of_limit_points {a b : Sequence} {c : ℝ} (hab : ∀ n ≥ b.m, a.LimitPoint (b.seq n)) (hbc : b.LimitPoint c) : a.LimitPoint c

Exercise 6.4.10