Аналіз I, Розділ 9.10: Границі на нескінченності
Я (прим. перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним підходом Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підправити", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.
Основні конструкції та результати цього розділу:
-
Базовий набір API для версій Mathlib щодо збіжності до нескінченності та границь на нескінченності.
namespace Chapter9
Визначення 9.10.1 (Нескінченна точка дотику). Ми використовуємо ¬ BddAbove X як позначення того, що є точкою дотику множини X.
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) = ⊤
X:Set ℝ⊢ (∀ (M : ℝ), ∃ x ∈ X, M < x) ↔ ∀ b < ⊤, ∃ a ∈ X, b < ↑a
X:Set ℝ⊢ (∀ (M : ℝ), ∃ x ∈ X, M < x) → ∀ b < ⊤, ∃ a ∈ X, b < ↑aX:Set ℝ⊢ (∀ b < ⊤, ∃ a ∈ X, b < ↑a) → ∀ (M : ℝ), ∃ x ∈ X, M < x
X:Set ℝ⊢ (∀ (M : ℝ), ∃ x ∈ X, M < x) → ∀ b < ⊤, ∃ a ∈ X, b < ↑a X:Set ℝh:∀ (M : ℝ), ∃ x ∈ X, M < xM:ERealhM:M < ⊤⊢ ∃ a ∈ X, M < ↑a; X:Set ℝh:∀ (M : ℝ), ∃ x ∈ X, M < xM:ERealhM:M < ⊤x:ℝhx:x ∈ XhxM:M.toReal < x⊢ ∃ a ∈ X, M < ↑a
X:Set ℝh:∀ (M : ℝ), ∃ x ∈ X, M < xM:ERealhM:M < ⊤x:ℝhx:x ∈ XhxM:M.toReal < x⊢ M < ↑x; X:Set ℝh:∀ (M : ℝ), ∃ x ∈ X, M < xx:ℝhx:x ∈ X⊢ ∀ M < ⊤, M.toReal < x → M < ↑x; All goals completed! 🐙
X:Set ℝh:∀ b < ⊤, ∃ a ∈ X, b < ↑aM:ℝ⊢ ∃ x ∈ X, M < x; X:Set ℝh:∀ b < ⊤, ∃ a ∈ X, b < ↑aM:ℝ⊢ ↑M < ⊤X:Set ℝM:ℝh:∃ a ∈ X, ↑M < ↑a⊢ ∃ x ∈ X, M < x X:Set ℝh:∀ b < ⊤, ∃ a ∈ X, b < ↑aM:ℝ⊢ ↑M < ⊤X:Set ℝM:ℝh:∃ a ∈ X, ↑M < ↑a⊢ ∃ x ∈ X, M < x 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 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! 🐙
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! 🐙Визначення 9.10.13 (Границя на нескінченності)
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! 🐙Вправа 9.10.4
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
/-- Вправа 9.10.1 -/
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