Analysis I, Section 9.10: Limits at infinity

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

Definition 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; choose x hx hxM using h M.toRealmpX:Set ℝh:∀ (M : ℝ), ∃ x ∈ X, M < xM:ERealhM:M < ⊤x:ℝhx:x ∈ XhxM:M.toReal < x⊢ ∃ a ∈ X, M < ↑a
    use x, hxrightX:Set ℝh:∀ (M : ℝ), ∃ x ∈ X, M < xM:ERealhM:M < ⊤x:ℝhx:x ∈ XhxM:M.toReal < x⊢ M < ↑x; revert MrightX:Set ℝh:∀ (M : ℝ), ∃ x ∈ X, M < xx:ℝhx:x ∈ X⊢ ∀ M < ⊤, M.toReal < x → M < ↑x; simp [EReal.forall]All goals completed! 🐙
  intro h MmprX:Set ℝh:∀ b < ⊤, ∃ a ∈ X, b < ↑aM:ℝ⊢ ∃ x ∈ X, M < x; specialize h (M:EReal) ?_mprX:Set ℝh:∀ b < ⊤, ∃ a ∈ X, b < ↑aM:ℝ⊢ ↑M < ⊤mprX:Set ℝM:ℝh:∃ a ∈ X, ↑M < ↑a⊢ ∃ x ∈ X, M < x <;>mprX:Set ℝh:∀ b < ⊤, ∃ a ∈ X, b < ↑aM:ℝ⊢ ↑M < ⊤mprX:Set ℝM:ℝh:∃ a ∈ X, ↑M < ↑a⊢ ∃ x ∈ X, M < x simp_allAll 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; choose x hx hxM using h M.toRealmpX:Set ℝh:∀ (M : ℝ), ∃ x ∈ X, x < MM:ERealhM:⊥ < Mx:ℝhx:x ∈ XhxM:x < M.toReal⊢ ∃ a ∈ X, ↑a < M
    use x, hxrightX:Set ℝh:∀ (M : ℝ), ∃ x ∈ X, x < MM:ERealhM:⊥ < Mx:ℝhx:x ∈ XhxM:x < M.toReal⊢ ↑x < M; revert MrightX:Set ℝh:∀ (M : ℝ), ∃ x ∈ X, x < Mx:ℝhx:x ∈ X⊢ ∀ (M : EReal), ⊥ < M → x < M.toReal → ↑x < M; simp [EReal.forall]All goals completed! 🐙
  intro h MmprX:Set ℝh:∀ (b : EReal), ⊥ < b → ∃ a ∈ X, ↑a < bM:ℝ⊢ ∃ x ∈ X, x < M; specialize h (M:EReal) ?_mprX:Set ℝh:∀ (b : EReal), ⊥ < b → ∃ a ∈ X, ↑a < bM:ℝ⊢ ⊥ < ↑MmprX:Set ℝM:ℝh:∃ a ∈ X, ↑a < ↑M⊢ ∃ x ∈ X, x < M <;>mprX:Set ℝh:∀ (b : EReal), ⊥ < b → ∃ a ∈ X, ↑a < bM:ℝ⊢ ⊥ < ↑MmprX:Set ℝM:ℝh:∃ a ∈ X, ↑a < ↑M⊢ ∃ x ∈ X, x < Msimp_allAll goals completed! 🐙

Definition 9.10.13 (Limit at infinity)

theorem Filter.Tendsto.AtTop.iff {X: Set ℝ} (f:ℝ → ℝ) (L:ℝ) : Filter.Tendsto f (.atTop ⊓ .principal X) (nhds L) ↔ ∀ ε > (0:ℝ), ∃ M, ∀ x ∈ X ∩ .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| < ε
  peel with ε 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]h.hX:Set ℝf:ℝ → ℝL:ℝε:ℝhε:ε > 0⊢ (∃ a, ∀ (b : ℝ), a ≤ b → b ∈ X → |f b - L| < ε) ↔ ∃ M, ∀ x ∈ X, M ≤ x → |f x - L| < ε
  aesopAll goals completed! 🐙

Exercise 9.10.4

declaration uses 'sorry'example : Filter.Tendsto (fun x:ℝ ↦ 1/x) (.atTop ⊓ .principal (.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
/-- Exercise 9.10.1 -/
declaration uses 'sorry'example (a:ℕ → ℝ) (L:ℝ) : Filter.Tendsto (fun x:ℝ ↦ (if h:(∃ n:ℕ, x = n) then a h.choose else 0)) (.atTop ⊓ .principal ((fun n:ℕ ↦ (n:ℝ)) '' .univ)) (nhds L) ↔ Filter.atTop.Tendsto a (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