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 being an adherent point
theorem BddAbove.unbounded_iff (X:Set ℝ) : ¬ BddAbove X ↔ ∀ M, ∃ x ∈ X, x > M := X:Set ℝ⊢ ¬BddAbove X ↔ ∀ (M : ℝ), ∃ x ∈ X, x > M
All goals completed! 🐙theorem BddAbove.unbounded_iff' (X:Set ℝ) : ¬ BddAbove X ↔ sSup ((fun x:ℝ ↦ (x:EReal)) '' X) = ⊤ := X:Set ℝ⊢ ¬BddAbove X ↔ sSup ((fun x => ↑x) '' X) = ⊤
erw [sSup_eq_top, unbounded_iffX:Set ℝ⊢ (∀ (M : ℝ), ∃ x ∈ X, x > M) ↔ ∀ b < ⊤, ∃ a ∈ (fun x => ↑x) '' X, b < a
X:Set ℝ⊢ (∀ (M : ℝ), ∃ x ∈ X, x > M) → ∀ b < ⊤, ∃ a ∈ (fun x => ↑x) '' X, b < aX:Set ℝ⊢ (∀ b < ⊤, ∃ a ∈ (fun x => ↑x) '' X, b < a) → ∀ (M : ℝ), ∃ x ∈ X, x > M
X:Set ℝ⊢ (∀ (M : ℝ), ∃ x ∈ X, x > M) → ∀ b < ⊤, ∃ a ∈ (fun x => ↑x) '' X, b < a intro h X:Set ℝh:∀ (M : ℝ), ∃ x ∈ X, x > MM:EReal⊢ M < ⊤ → ∃ a ∈ (fun x => ↑x) '' X, M < a X:Set ℝh:∀ (M : ℝ), ∃ x ∈ X, x > MM:ERealhM:M < ⊤⊢ ∃ a ∈ (fun x => ↑x) '' X, M < a; X:Set ℝh:∀ (M : ℝ), ∃ x ∈ X, x > MM:ERealhM:M < ⊤x:ℝhx:x ∈ XhxM:x > M.toReal⊢ ∃ a ∈ (fun x => ↑x) '' X, M < a
X:Set ℝh:∀ (M : ℝ), ∃ x ∈ X, x > MM:ERealhM:M < ⊤x:ℝhx:x ∈ XhxM:x > M.toReal⊢ M < ↑x; X:Set ℝh:∀ (M : ℝ), ∃ x ∈ X, x > Mx:ℝhx:x ∈ X⊢ ∀ M < ⊤, x > M.toReal → M < ↑x; X:Set ℝh:∀ (M : ℝ), ∃ x ∈ X, x > Mx:ℝhx:x ∈ X⊢ ⊤ < ⊤ → 0 < x → ⊤ < ↑x; All goals completed! 🐙
intro h X:Set ℝh:∀ b < ⊤, ∃ a ∈ (fun x => ↑x) '' X, b < aM:ℝ⊢ ∃ x ∈ X, x > M; X:Set ℝM:ℝh:∃ a ∈ (fun x => ↑x) '' X, ↑M < a⊢ ∃ x ∈ X, x > M
X:Set ℝM:ℝx:ℝhx:x ∈ XhMx:↑M < (fun x => ↑x) x⊢ ∃ x ∈ X, x > M; All goals completed! 🐙theorem BddBelow.unbounded_iff (X:Set ℝ) : ¬ BddBelow X ↔ ∀ M, ∃ x ∈ X, x < M := X:Set ℝ⊢ ¬BddBelow X ↔ ∀ (M : ℝ), ∃ x ∈ X, x < M
All goals completed! 🐙theorem BddBelow.unbounded_iff' (X:Set ℝ) : ¬ BddBelow X ↔ sInf ((fun x:ℝ ↦ (x:EReal)) '' X) = ⊥ := X:Set ℝ⊢ ¬BddBelow X ↔ sInf ((fun x => ↑x) '' X) = ⊥
X:Set ℝ⊢ (∀ (M : ℝ), ∃ x ∈ X, x < M) ↔ ∀ (b : EReal), ⊥ < b → ∃ a ∈ X, ↑a < b
X:Set ℝ⊢ (∀ (M : ℝ), ∃ x ∈ X, x < M) → ∀ (b : EReal), ⊥ < b → ∃ a ∈ X, ↑a < bX:Set ℝ⊢ (∀ (b : EReal), ⊥ < b → ∃ a ∈ X, ↑a < b) → ∀ (M : ℝ), ∃ x ∈ X, x < M
X:Set ℝ⊢ (∀ (M : ℝ), ∃ x ∈ X, x < M) → ∀ (b : EReal), ⊥ < b → ∃ a ∈ X, ↑a < b intro h X:Set ℝh:∀ (M : ℝ), ∃ x ∈ X, x < MM:EReal⊢ ⊥ < M → ∃ a ∈ X, ↑a < M X:Set ℝh:∀ (M : ℝ), ∃ x ∈ X, x < MM:ERealhM:⊥ < M⊢ ∃ a ∈ X, ↑a < M; X:Set ℝh:∀ (M : ℝ), ∃ x ∈ X, x < MM:ERealhM:⊥ < Mx:ℝhx:x ∈ XhxM:x < M.toReal⊢ ∃ a ∈ X, ↑a < M
X:Set ℝh:∀ (M : ℝ), ∃ x ∈ X, x < MM:ERealhM:⊥ < Mx:ℝhx:x ∈ XhxM:x < M.toReal⊢ ↑x < M; X:Set ℝh:∀ (M : ℝ), ∃ x ∈ X, x < Mx:ℝhx:x ∈ X⊢ ∀ (M : EReal), ⊥ < M → x < M.toReal → ↑x < M; All goals completed! 🐙
intro h X:Set ℝh:∀ (b : EReal), ⊥ < b → ∃ a ∈ X, ↑a < bM:ℝ⊢ ∃ x ∈ X, x < M; X:Set ℝh:∀ (b : EReal), ⊥ < b → ∃ a ∈ X, ↑a < bM:ℝ⊢ ⊥ < ↑MX:Set ℝM:ℝh:∃ a ∈ X, ↑a < ↑M⊢ ∃ x ∈ X, x < M X:Set ℝh:∀ (b : EReal), ⊥ < b → ∃ a ∈ X, ↑a < bM:ℝ⊢ ⊥ < ↑MX:Set ℝM:ℝh:∃ a ∈ X, ↑a < ↑M⊢ ∃ x ∈ X, x < MAll 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| < ε := X:Set ℝf:ℝ → ℝL:ℝ⊢ Filter.Tendsto f (Filter.atTop ⊓ Filter.principal X) (nhds L) ↔ ∀ ε > 0, ∃ M, ∀ x ∈ X ∩ Set.Ici M, |f x - L| < ε
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| < ε
X:Set ℝf:ℝ → ℝL:ℝε:ℝhε:ε > 0⊢ (∀ᶠ (b : ℝ) in Filter.atTop ⊓ Filter.principal X, |f b - L| < ε) ↔ ∃ M, ∀ x ∈ X ∩ Set.Ici M, |f x - L| < ε
X:Set ℝf:ℝ → ℝL:ℝε:ℝhε:ε > 0⊢ (∃ a, ∀ (b : ℝ), a ≤ b → b ∈ X → |f b - L| < ε) ↔ ∃ M, ∀ x ∈ X, M ≤ x → |f x - L| < ε
All goals completed! 🐙Exercise 9.10.4
declaration uses `sorry`example : Filter.Tendsto (fun x:ℝ ↦ 1/x) (.atTop ⊓ .principal (.Ioi 0)) (nhds 0) := ⊢ Filter.Tendsto (fun x => 1 / x) (Filter.atTop ⊓ Filter.principal (Set.Ioi 0)) (nhds 0)
All 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) := 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)
All goals completed! 🐙end Chapter9