Аналіз 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:

namespace Chapter6

Визначення 6.6.1

abbrev Sequence.subseq (a b: ℕ → ℝ) : Prop := ∃ f : ℕ → ℕ, StrictMono f ∧ ∀ n, b n = a (f n)
/- Example 6.6.2 -/ declaration uses 'sorry'example (a:ℕ → ℝ) : Sequence.subseq a (fun n ↦ a (2 * n)) := a:ℕ → ℝ⊢ Sequence.subseq a fun n => a (2 * n) All goals completed! 🐙declaration uses 'sorry'example {f: ℕ → ℕ} (hf: StrictMono f) : Function.Injective f := f:ℕ → ℕhf:StrictMono f⊢ Function.Injective f All goals completed! 🐙declaration uses 'sorry'example : Sequence.subseq (fun n ↦ if Even n then 1 + (10:ℝ)^(-(n/2:ℤ)-1) else (1:ℝ)^(-(n/2:ℤ)-1)) (fun n ↦ 1 + (10:ℝ)^(-(n:ℤ)-1)) := ⊢ Sequence.subseq (fun n => if Even n then 1 + 10 ^ (-(↑n / 2) - 1) else 1 ^ (-(↑n / 2) - 1)) fun n => 1 + 10 ^ (-↑n - 1) All goals completed! 🐙declaration uses 'sorry'example : Sequence.subseq (fun n ↦ if Even n then 1 + (10:ℝ)^(-(n/2:ℤ)-1) else (1:ℝ)^(-(n/2:ℤ)-1)) (fun n ↦ (10:ℝ)^(-(n:ℤ)-1)) := ⊢ Sequence.subseq (fun n => if Even n then 1 + 10 ^ (-(↑n / 2) - 1) else 1 ^ (-(↑n / 2) - 1)) fun n => 10 ^ (-↑n - 1) All goals completed! 🐙

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

theorem declaration uses 'sorry'Sequence.subseq_self (a:ℕ → ℝ) : Sequence.subseq a a := a:ℕ → ℝ⊢ subseq a a All goals completed! 🐙

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

theorem declaration uses 'sorry'Sequence.subseq_trans {a b c:ℕ → ℝ} (hab: Sequence.subseq a b) (hbc: Sequence.subseq b c) : Sequence.subseq a c := a:ℕ → ℝb:ℕ → ℝc:ℕ → ℝhab:subseq a bhbc:subseq b c⊢ subseq a c All goals completed! 🐙

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

theorem declaration uses 'sorry'Sequence.convergent_iff_subseq (a:ℕ → ℝ) (L:ℝ) : (a:Sequence).tendsTo L ↔ ∀ b:ℕ → ℝ, Sequence.subseq a b → (b:Sequence).tendsTo L := 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 All goals completed! 🐙

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

theorem declaration uses 'sorry'Sequence.limit_point_iff_subseq (a:ℕ → ℝ) (L:ℝ) : (a:Sequence).limit_point L ↔ ∃ b:ℕ → ℝ, Sequence.subseq a b ∧ (b:Sequence).tendsTo L := 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 All goals completed! 🐙

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

theorem Sequence.convergent_of_subseq_of_bounded {a:ℕ→ ℝ} (ha: (a:Sequence).isBounded) : ∃ b:ℕ → ℝ, Sequence.subseq a b ∧ (b:Sequence).convergent := 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 -- цей доказ написан так, щоб співпадати із структурою орігінального тексту. a:ℕ → ℝha:{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isBoundedL_plus:ℝhL_plus:{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.limsup = ↑L_plusL_minus:ℝhL_minus:{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.liminf = ↑L_minus⊢ ∃ b, subseq a b ∧ { m := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.convergent a:ℕ → ℝha:{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isBoundedL_plus:ℝhL_plus:{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.limsup = ↑L_plusL_minus:ℝhL_minus:{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.liminf = ↑L_minusthis:{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.limit_point L_plus⊢ ∃ b, subseq a b ∧ { m := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.convergent a:ℕ → ℝha:{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isBoundedL_plus:ℝhL_plus:{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.limsup = ↑L_plusL_minus:ℝhL_minus:{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.liminf = ↑L_minusthis:∃ b, subseq a b ∧ { m := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.tendsTo L_plus⊢ ∃ b, subseq a b ∧ { m := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.convergent a:ℕ → ℝha:{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isBoundedL_plus:ℝhL_plus:{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.limsup = ↑L_plusL_minus:ℝhL_minus:{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.liminf = ↑L_minusb:ℕ → ℝhsubseq:subseq a bhtends:{ m := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.tendsTo L_plus⊢ ∃ b, subseq a b ∧ { m := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.convergent All goals completed! 🐙
/- Вправа 6.6.2 -/ def declaration uses 'sorry'Sequence.exist_subseq_of_subseq : Decidable (∃ a b : ℕ → ℝ, a ≠ b ∧ Sequence.subseq a b ∧ Sequence.subseq b a) := ⊢ Decidable (∃ a b, a ≠ b ∧ subseq a b ∧ subseq b a) -- The first line of this construction should be `apply isTrue` or `apply isFalse`. All goals completed! 🐙

Вправа 6.6.3. You may find the API around Mathlib's Nat.find {p : ℕ → Prop} [DecidablePred p] (H : ∃ n, p n) : ℕNat.find to be useful (and to avoid any decidability issues)

theorem declaration uses 'sorry'Sequence.subseq_of_unbounded {a:ℕ → ℝ} (ha: ¬ (a:Sequence).isBounded) : ∃ b:ℕ → ℝ, Sequence.subseq a b ∧ (b:Sequence)⁻¹.tendsTo 0 := 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 All goals completed! 🐙
end Chapter6