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

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:

Bare-bones API for the Mathlib versions of adherent at infinity, and limits at infinity.

namespace Chapter9

Визначення 9.10.1 (Infinite adherent point). We use ¬BddAbove sorry : Prop¬ BddAbove unknown identifier 'X'X as our notation for being an adherent point

theorem BddAbove.unbounded_iff (X:Set ℝ) : ¬ BddAbove X ↔ ∀ M, ∃ x ∈ X, x > M := byX:Set ℝ⊢ ¬BddAbove X ↔ ∀ (M : ℝ), ∃ x ∈ X, x > M
  simp [bddAbove_def]All goals completed! 🐙

theorem BddAbove.unbounded_iff' (X:Set ℝ) : ¬ BddAbove X ↔ sSup ((fun x:ℝ ↦ (x:EReal)) '' X) = ⊤ := byX:Set ℝ⊢ ¬BddAbove X ↔ sSup ((fun x => ↑x) '' X) = ⊤
  simp [sSup_eq_top, unbounded_iff]X:Set ℝ⊢ (∀ (M : ℝ), ∃ x ∈ X, M < x) ↔ ∀ b < ⊤, ∃ a ∈ X, b < ↑a
  constructormpX:Set ℝ⊢ (∀ (M : ℝ), ∃ x ∈ X, M < x) → ∀ b < ⊤, ∃ a ∈ X, b < ↑amprX:Set ℝ⊢ (∀ b < ⊤, ∃ a ∈ X, b < ↑a) → ∀ (M : ℝ), ∃ x ∈ X, M < x
  .mpX:Set ℝ⊢ (∀ (M : ℝ), ∃ x ∈ X, M < x) → ∀ b < ⊤, ∃ a ∈ X, b < ↑a intro h M hMmpX:Set ℝh:∀ (M : ℝ), ∃ x ∈ X, M < xM:ERealhM:M < ⊤⊢ ∃ a ∈ X, M < ↑a
    specialize h M.toRealmpX:Set ℝM:ERealhM:M < ⊤h:∃ x ∈ X, M.toReal < x⊢ ∃ a ∈ X, M < ↑a
    obtain ⟨ x, hx, hxM ⟩ := hmp.intro.introX:Set ℝM:ERealhM:M < ⊤x:ℝhx:x ∈ XhxM:M.toReal < x⊢ ∃ a ∈ X, M < ↑a
    use x, hxrightX:Set ℝM:ERealhM:M < ⊤x:ℝhx:x ∈ XhxM:M.toReal < x⊢ M < ↑x
    revert MrightX:Set ℝx:ℝhx:x ∈ X⊢ ∀ M < ⊤, M.toReal < x → M < ↑x
    rw [EReal.forall]rightX:Set ℝx:ℝhx:x ∈ X⊢ (⊥ < ⊤ → ⊥.toReal < x → ⊥ < ↑x) ∧ (⊤ < ⊤ → ⊤.toReal < x → ⊤ < ↑x) ∧ ∀ (r : ℝ), ↑r < ⊤ → (↑r).toReal < x → ↑r < ↑x
    simpAll goals completed! 🐙
  intro h MmprX:Set ℝh:∀ b < ⊤, ∃ a ∈ X, b < ↑aM:ℝ⊢ ∃ x ∈ X, M < x
  specialize h (M:EReal) (byX:Set ℝh:∀ b < ⊤, ∃ a ∈ X, b < ↑aM:ℝ⊢ ↑M < ⊤ simpAll goals completed! 🐙)
  simp at hmprX:Set ℝM:ℝh:∃ a ∈ X, M < a⊢ ∃ x ∈ X, M < x
  exact hAll goals completed! 🐙

theorem BddBelow.unbounded_iff (X:Set ℝ) : ¬ BddBelow X ↔ ∀ M, ∃ x ∈ X, x < M := byX:Set ℝ⊢ ¬BddBelow X ↔ ∀ (M : ℝ), ∃ x ∈ X, x < M
  simp [bddBelow_def]All goals completed! 🐙

theorem BddBelow.unbounded_iff' (X:Set ℝ) : ¬ BddBelow X ↔ sInf ((fun x:ℝ ↦ (x:EReal)) '' X) = ⊥ := byX:Set ℝ⊢ ¬BddBelow X ↔ sInf ((fun x => ↑x) '' X) = ⊥
  simp [sInf_eq_bot, unbounded_iff]X:Set ℝ⊢ (∀ (M : ℝ), ∃ x ∈ X, x < M) ↔ ∀ (b : EReal), ⊥ < b → ∃ a ∈ X, ↑a < b
  constructormpX:Set ℝ⊢ (∀ (M : ℝ), ∃ x ∈ X, x < M) → ∀ (b : EReal), ⊥ < b → ∃ a ∈ X, ↑a < bmprX:Set ℝ⊢ (∀ (b : EReal), ⊥ < b → ∃ a ∈ X, ↑a < b) → ∀ (M : ℝ), ∃ x ∈ X, x < M
  .mpX:Set ℝ⊢ (∀ (M : ℝ), ∃ x ∈ X, x < M) → ∀ (b : EReal), ⊥ < b → ∃ a ∈ X, ↑a < b intro h M hMmpX:Set ℝh:∀ (M : ℝ), ∃ x ∈ X, x < MM:ERealhM:⊥ < M⊢ ∃ a ∈ X, ↑a < M
    specialize h M.toRealmpX:Set ℝM:ERealhM:⊥ < Mh:∃ x ∈ X, x < M.toReal⊢ ∃ a ∈ X, ↑a < M
    obtain ⟨ x, hx, hxM ⟩ := hmp.intro.introX:Set ℝM:ERealhM:⊥ < Mx:ℝhx:x ∈ XhxM:x < M.toReal⊢ ∃ a ∈ X, ↑a < M
    use x, hxrightX:Set ℝM:ERealhM:⊥ < Mx:ℝhx:x ∈ XhxM:x < M.toReal⊢ ↑x < M
    revert MrightX:Set ℝx:ℝhx:x ∈ X⊢ ∀ (M : EReal), ⊥ < M → x < M.toReal → ↑x < M
    rw [EReal.forall]rightX:Set ℝx:ℝhx:x ∈ X⊢ (⊥ < ⊥ → x < ⊥.toReal → ↑x < ⊥) ∧ (⊥ < ⊤ → x < ⊤.toReal → ↑x < ⊤) ∧ ∀ (r : ℝ), ⊥ < ↑r → x < (↑r).toReal → ↑x < ↑r
    simpAll goals completed! 🐙
  intro h MmprX:Set ℝh:∀ (b : EReal), ⊥ < b → ∃ a ∈ X, ↑a < bM:ℝ⊢ ∃ x ∈ X, x < M
  specialize h (M:EReal) (byX:Set ℝh:∀ (b : EReal), ⊥ < b → ∃ a ∈ X, ↑a < bM:ℝ⊢ ⊥ < ↑M simpAll goals completed! 🐙)
  simp at hmprX:Set ℝM:ℝh:∃ a ∈ X, a < M⊢ ∃ x ∈ X, x < M
  exact hAll goals completed! 🐙

Визначення 9.10.13 (Limit at infinity)

theorem Filter.Tendsto.AtTop.iff {X: Set ℝ} (f:ℝ → ℝ) (L:ℝ) : Filter.Tendsto f (Filter.atTop ⊓ Filter.principal X) (nhds L) ↔ ∀ ε > (0:ℝ), ∃ M, ∀ x ∈ X ∩ Set.Ici M, |f x - L| < ε := byX:Set ℝf:ℝ → ℝL:ℝ⊢ Filter.Tendsto f (Filter.atTop ⊓ Filter.principal X) (nhds L) ↔ ∀ ε > 0, ∃ M, ∀ x ∈ X ∩ Set.Ici M, |f x - L| < ε
  rw [LinearOrderedAddCommGroup.tendsto_nhds]X:Set ℝf:ℝ → ℝL:ℝ⊢ (∀ ε > 0, ∀ᶠ (b : ℝ) in Filter.atTop ⊓ Filter.principal X, |f b - L| < ε) ↔
  ∀ ε > 0, ∃ M, ∀ x ∈ X ∩ Set.Ici M, |f x - L| < ε
  apply forall_congr'hX:Set ℝf:ℝ → ℝL:ℝ⊢ ∀ (a : ℝ),
  (a > 0 → ∀ᶠ (b : ℝ) in Filter.atTop ⊓ Filter.principal X, |f b - L| < a) ↔
    a > 0 → ∃ M, ∀ x ∈ X ∩ Set.Ici M, |f x - L| < a; intro εhX:Set ℝf:ℝ → ℝL:ℝε:ℝ⊢ (ε > 0 → ∀ᶠ (b : ℝ) in Filter.atTop ⊓ Filter.principal X, |f b - L| < ε) ↔
  ε > 0 → ∃ M, ∀ x ∈ X ∩ Set.Ici M, |f x - L| < ε
  apply imp_congr_righth.hX:Set ℝf:ℝ → ℝL:ℝε:ℝ⊢ ε > 0 → ((∀ᶠ (b : ℝ) in Filter.atTop ⊓ Filter.principal X, |f b - L| < ε) ↔ ∃ M, ∀ x ∈ X ∩ Set.Ici M, |f x - L| < ε); intro hεh.hX:Set ℝf:ℝ → ℝL:ℝε:ℝhε:ε > 0⊢ (∀ᶠ (b : ℝ) in Filter.atTop ⊓ Filter.principal X, |f b - L| < ε) ↔ ∃ M, ∀ x ∈ X ∩ Set.Ici M, |f x - L| < ε
  simp [Filter.eventually_inf_principal, Filter.eventually_atTop]h.hX:Set ℝf:ℝ → ℝL:ℝε:ℝhε:ε > 0⊢ (∃ a, ∀ (b : ℝ), a ≤ b → b ∈ X → |f b - L| < ε) ↔ ∃ M, ∀ x ∈ X, M ≤ x → |f x - L| < ε
  apply exists_congrh.h.hX:Set ℝf:ℝ → ℝL:ℝε:ℝhε:ε > 0⊢ ∀ (a : ℝ), (∀ (b : ℝ), a ≤ b → b ∈ X → |f b - L| < ε) ↔ ∀ x ∈ X, a ≤ x → |f x - L| < ε; intro Mh.h.hX:Set ℝf:ℝ → ℝL:ℝε:ℝhε:ε > 0M:ℝ⊢ (∀ (b : ℝ), M ≤ b → b ∈ X → |f b - L| < ε) ↔ ∀ x ∈ X, M ≤ x → |f x - L| < ε
  apply forall_congr'h.h.h.hX:Set ℝf:ℝ → ℝL:ℝε:ℝhε:ε > 0M:ℝ⊢ ∀ (a : ℝ), M ≤ a → a ∈ X → |f a - L| < ε ↔ a ∈ X → M ≤ a → |f a - L| < ε; intro xh.h.h.hX:Set ℝf:ℝ → ℝL:ℝε:ℝhε:ε > 0M:ℝx:ℝ⊢ M ≤ x → x ∈ X → |f x - L| < ε ↔ x ∈ X → M ≤ x → |f x - L| < ε
  tautoAll goals completed! 🐙

Вправа 9.10.4

declaration uses 'sorry'example : Filter.Tendsto (fun x:ℝ ↦ 1/x) (Filter.atTop ⊓ Filter.principal (Set.Ioi 0)) (nhds 0) := by⊢ Filter.Tendsto (fun x => 1 / x) (Filter.atTop ⊓ Filter.principal (Set.Ioi 0)) (nhds 0)
  sorryAll goals completed! 🐙

open Classical in
/-- Вправа 9.10.1 -/
declaration uses 'sorry'example (a:ℕ → ℝ) (L:ℝ) : Filter.Tendsto (fun x:ℝ ↦ (if h:(∃ n:ℕ, x = n) then a h.choose else 0)) (Filter.atTop ⊓ Filter.principal ((fun n:ℕ ↦ (n:ℝ)) '' Set.univ)) (nhds L) ↔ Filter.Tendsto a Filter.atTop (nhds L) := bya:ℕ → ℝL:ℝ⊢ Filter.Tendsto (fun x => if h : ∃ n, x = ↑n then a h.choose else 0)
    (Filter.atTop ⊓ Filter.principal ((fun n => ↑n) '' Set.univ)) (nhds L) ↔
  Filter.Tendsto a Filter.atTop (nhds L)
  sorryAll goals completed! 🐙

end Chapter9