Analysis I, Section 6.6: Subsequences

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.

namespace Chapter6

Definition 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)) := 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 (1:ℝ)^(-(n/2:ℤ)-1))
    (fun n ↦ 1 + (10:ℝ)^(-(n:ℤ)-1)) := by⊢ Sequence.subseq (fun n => if Even n then 1 + 10 ^ (-(↑n / 2) - 1) else 1 ^ (-(↑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 (1:ℝ)^(-(n/2:ℤ)-1))
    (fun n ↦ (10:ℝ)^(-(n:ℤ)-1)) := by⊢ Sequence.subseq (fun n => if Even n then 1 + 10 ^ (-(↑n / 2) - 1) else 1 ^ (-(↑n / 2) - 1)) fun n => 10 ^ (-↑n - 1)
  sorryAll goals completed! 🐙

Lemma 6.6.4 / Exercise 6.6.1

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

Lemma 6.6.4 / Exercise 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! 🐙

Proposition 6.6.5 / Exercise 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! 🐙

Proposition 6.6.6 / Exercise 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! 🐙

Theorem 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 := bya:ℕ → ℝha:(↑a).IsBounded⊢ ∃ b, subseq a b ∧ (↑b).Convergent
  -- This proof is written to follow the structure of the original text.
  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! 🐙

/- Exercise 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)
    -- The first line of this construction should be `apply isTrue` or `apply isFalse`.
    sorryAll goals completed! 🐙

Exercise 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 := bya:ℕ → ℝha:¬(↑a).IsBounded⊢ ∃ b, subseq a b ∧ (↑b)⁻¹.TendsTo 0
  sorryAll goals completed! 🐙

end Chapter6