Аналіз I, Глава 6.4

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.continually_adherent (ε : ℝ) (a : Chapter6.Sequence) (x : ℝ) : Prop

Equations

• ε.continually_adherent a x = ∀ N ≥ a.m, ε.adherent (a.from N) x

@[reducible, inline]

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

Equations

• a.limit_point x = ∀ ε > 0, ε.continually_adherent a x

theorem Chapter6.Sequence.limit_point_def (a : Sequence) (x : ℝ) : a.limit_point 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 = { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => 1 - 10 ^ (-↑n - 1)) n.toNat else 0, vanish := Chapter6.Example_6_4_3._proof_2 }

@[reducible, inline]

noncomputable abbrev Chapter6.Example_6_4_4 : Sequence

Equations

• Chapter6.Example_6_4_4 = { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => (-1) ^ n * (1 + 10 ^ (-↑n - 1))) n.toNat else 0, vanish := Chapter6.Example_6_4_4._proof_3 }

theorem Chapter6.Sequence.limit_point_of_limit {a : Sequence} {x : ℝ} (h : a.tendsTo x) : a.limit_point x

Твердження 6.4.5 / Вправа 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 = { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => (-1) ^ n * (1 + 10 ^ (-↑n - 1))) n.toNat else 0, vanish := Chapter6.Example_6_4_4._proof_3 }

@[reducible, inline]

noncomputable abbrev Chapter6.Example_6_4_8 : Sequence

Equations

• Chapter6.Example_6_4_8 = { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => if Even n then ↑n + 1 else -↑n - 1) n.toNat else 0, vanish := Chapter6.Example_6_4_8._proof_4 }

@[reducible, inline]

noncomputable abbrev Chapter6.Example_6_4_9 : Sequence

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev Chapter6.Example_6_4_10 : Sequence

Equations

• Chapter6.Example_6_4_10 = { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => ↑n + 1) n.toNat else 0, vanish := Chapter6.Example_6_4_10._proof_6 }

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

Твердження 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

Твердження 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

Твердження 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

Твердження 6.4.12(b)

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

Твердження 6.4.12(c) / Вправа 6.4.3

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

Твердження 6.4.12(c) / Вправа 6.4.3

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

Твердження 6.4.12(c) / Вправа 6.4.3

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

Твердження 6.4.12(d) / Вправа 6.4.3

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

Твердження 6.4.12(e) / Вправа 6.4.3

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

Твердження 6.4.12(e) / Вправа 6.4.3

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

Твердження 6.4.12(f) / Вправа 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

Лема 6.4.13 (Comparison principle) / Вправа 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

Лема 6.4.13 (Comparison principle) / Вправа 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

Лема 6.4.13 (Comparison principle) / Вправа 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

Лема 6.4.13 (Comparison principle) / Вправа 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

Наслідок 6.4.14 (Squeeze test) / Вправа 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

Наслідок 6.4.17 (Zero test for sequences) / Вправа 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

Теорема 6.4.18 (Completeness of the reals)

theorem Chapter6.Sequence.sup_not_strict_mono : ∃ (a : ℕ → ℝ) (b : ℕ → ℝ), (∀ (n : ℕ), a n < b n) ∧ { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.sup ≠ { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.sup

Вправа 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.extended_limit_point (a : Sequence) (x : EReal) : Prop

This definition is needed for Exercises 6.4.8 and 6.4.9.

Equations

• a.extended_limit_point x = if x = ⊤ then ¬a.bddAbove else if x = ⊥ then ¬a.bddBelow else a.limit_point x.toReal

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

Вправа 6.4.8

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

Вправа 6.4.8

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

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

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

Вправа 6.4.9

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

Вправа 6.4.10