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

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 a subsequence

@[reducible, inline]

abbrev Chapter6.Sequence.subseq (a b : ℕ → ℝ) : Prop

Визначення 6.6.1

Equations

• Chapter6.Sequence.subseq a b = ∃ (f : ℕ → ℕ), StrictMono f ∧ ∀ (n : ℕ), b n = a (f n)

theorem Chapter6.Sequence.subseq_self (a : ℕ → ℝ) : subseq a a

Лема 6.6.4 / Вправа 6.6.1

theorem Chapter6.Sequence.subseq_trans {a b c : ℕ → ℝ} (hab : subseq a b) (hbc : subseq b c) : subseq a c

Лема 6.6.4 / Вправа 6.6.1

theorem Chapter6.Sequence.convergent_iff_subseq (a : ℕ → ℝ) (L : ℝ) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.tendsTo L ↔ ∀ (b : ℕ → ℝ), subseq a b → { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.tendsTo L

Твердження 6.6.5 / Вправа 6.6.4

theorem Chapter6.Sequence.limit_point_iff_subseq (a : ℕ → ℝ) (L : ℝ) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.limit_point L ↔ ∃ (b : ℕ → ℝ), subseq a b ∧ { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.tendsTo L

Твердження 6.6.6 / Вправа 6.6.5

theorem Chapter6.Sequence.convergent_of_subseq_of_bounded {a : ℕ → ℝ} (ha : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isBounded) : ∃ (b : ℕ → ℝ), subseq a b ∧ { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.convergent

Теорема 6.6.8 (Bolzano-Weierstrass theorem)

def Chapter6.Sequence.exist_subseq_of_subseq : Decidable (∃ (a : ℕ → ℝ) (b : ℕ → ℝ), a ≠ b ∧ subseq a b ∧ subseq b a)

Equations

• Chapter6.Sequence.exist_subseq_of_subseq = sorry

theorem Chapter6.Sequence.subseq_of_unbounded {a : ℕ → ℝ} (ha : ¬{ m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isBounded) : ∃ (b : ℕ → ℝ), subseq a b ∧ { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }⁻¹.tendsTo 0

Вправа 6.6.3. You may find the API around Mathlib's Nat.find to be useful (and open Classical to avoid any decidability issues)