Аналіз I, Розділ 6.6: Підпослідовності

Я (прим. перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним підходом Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підправити", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.

Основні конструкції та результати цього розділу:

Визначення підпослідовності.

namespace Chapter6

Визначення 6.6.1

abbrev Sequence.subseq (a b: ℕ → ℝ) : Prop := ∃ f : ℕ → ℕ, StrictMono f ∧ ∀ n, b n = a (f n)

/- Приклад 6.6.2 -/
declaration uses 'sorry'example (a:ℕ → ℝ) : Sequence.subseq a (fun n ↦ a (2 * n)) := bya:ℕ → ℝ⊢ Sequence.subseq a fun n => a (2 * n) sorryAll goals completed! 🐙

declaration uses 'sorry'example {f: ℕ → ℕ} (hf: StrictMono f) : Function.Injective f := byf:ℕ → ℕhf:StrictMono f⊢ Function.Injective f sorryAll goals completed! 🐙

declaration uses 'sorry'example :
    Sequence.subseq (fun n ↦ if Even n then 1 + (10:ℝ)^(-(n/2:ℤ)-1) else (10:ℝ)^(-(n/2:ℤ)-1))
    (fun n ↦ 1 + (10:ℝ)^(-(n:ℤ)-1)) := by⊢ Sequence.subseq (fun n => if Even n then 1 + 10 ^ (-(↑n / 2) - 1) else 10 ^ (-(↑n / 2) - 1)) fun n => 1 + 10 ^ (-↑n - 1)
  sorryAll goals completed! 🐙

declaration uses 'sorry'example :
    Sequence.subseq (fun n ↦ if Even n then 1 + (10:ℝ)^(-(n/2:ℤ)-1) else (10:ℝ)^(-(n/2:ℤ)-1))
    (fun n ↦ (10:ℝ)^(-(n:ℤ)-1)) := by⊢ Sequence.subseq (fun n => if Even n then 1 + 10 ^ (-(↑n / 2) - 1) else 10 ^ (-(↑n / 2) - 1)) fun n => 10 ^ (-↑n - 1)
  sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'Sequence.subseq_self (a:ℕ → ℝ) : Sequence.subseq a a := bya:ℕ → ℝ⊢ subseq a a sorryAll 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 := bya:ℕ → ℝb:ℕ → ℝc:ℕ → ℝhab:subseq a bhbc:subseq b c⊢ subseq a c sorryAll 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 := bya:ℕ → ℝL:ℝ⊢ (↑a).TendsTo L ↔ ∀ (b : ℕ → ℝ), subseq a b → (↑b).TendsTo L
  sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'Sequence.limit_point_iff_subseq (a:ℕ → ℝ) (L:ℝ) :
    (a:Sequence).LimitPoint L ↔ ∃ b:ℕ → ℝ, Sequence.subseq a b ∧ (b:Sequence).TendsTo L := bya:ℕ → ℝL:ℝ⊢ (↑a).LimitPoint L ↔ ∃ b, subseq a b ∧ (↑b).TendsTo L
  sorryAll goals completed! 🐙

Теорема 6.6.8 (Теорема Болцано-Вейерштрасса)

theorem Sequence.convergent_of_subseq_of_bounded {a:ℕ→ ℝ} (ha: (a:Sequence).IsBounded) :
    ∃ b:ℕ → ℝ, Sequence.subseq a b ∧ (b:Sequence).Convergent := bya:ℕ → ℝha:(↑a).IsBounded⊢ ∃ b, subseq a b ∧ (↑b).Convergent
  -- Доведення написане так, щоб відповідати структурі оригінального тексту.
  obtain ⟨ ⟨ L_plus, hL_plus ⟩, ⟨ _, _ ⟩ ⟩ := finite_limsup_liminf_of_bounded haintro.intro.introa:ℕ → ℝha:(↑a).IsBoundedL_plus:ℝhL_plus:(↑a).limsup = ↑L_plusw✝:ℝh✝:(↑a).liminf = ↑w✝⊢ ∃ b, subseq a b ∧ (↑b).Convergent
  have := limit_point_of_limsup hL_plusintro.intro.introa:ℕ → ℝha:(↑a).IsBoundedL_plus:ℝhL_plus:(↑a).limsup = ↑L_plusw✝:ℝh✝:(↑a).liminf = ↑w✝this:?_mvar.2454 := Chapter6.Sequence.limit_point_of_limsup _fvar.2432⊢ ∃ b, subseq a b ∧ (↑b).Convergent
  rw [limit_point_iff_subseq] at thisintro.intro.introa:ℕ → ℝha:(↑a).IsBoundedL_plus:ℝhL_plus:(↑a).limsup = ↑L_plusw✝:ℝh✝:(↑a).liminf = ↑w✝this:∃ b, subseq a b ∧ (↑b).TendsTo L_plus⊢ ∃ b, subseq a b ∧ (↑b).Convergent; peel 2 thisintro.intro.intro.h.ha:ℕ → ℝha:(↑a).IsBoundedL_plus:ℝhL_plus:(↑a).limsup = ↑L_plusw✝:ℝh✝:(↑a).liminf = ↑w✝this✝:∃ b, subseq a b ∧ (↑b).TendsTo L_plusb✝:ℕ → ℝp✝:subseq a b✝this:(↑b✝).TendsTo L_plus⊢ (↑b✝).Convergent; solve_by_elimAll 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) := by⊢ Decidable (∃ a b, a ≠ b ∧ subseq a b ∧ subseq b a)
    -- Перший рядок цієї конструкції має бути `apply isTrue` або `apply isFalse`.
    sorryAll goals completed! 🐙

Вправа 6.6.3. Може стати в пригоді API Nat.find {p : ℕ → Prop} [DecidablePred p] (H : ∃ n, p n) : ℕNat.find з Mathlib (та , щоб уникнути проблем з вирішуваністю).

theorem declaration uses 'sorry'Sequence.subseq_of_unbounded {a:ℕ → ℝ} (ha: ¬ (a:Sequence).IsBounded) :
    ∃ b:ℕ → ℝ, Sequence.subseq a b ∧ (b:Sequence)⁻¹.TendsTo 0 := bya:ℕ → ℝha:¬(↑a).IsBounded⊢ ∃ b, subseq a b ∧ (↑b)⁻¹.TendsTo 0
  sorryAll goals completed! 🐙

end Chapter6