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

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:

Technical point: in the text, the functions unknown identifier 'f'f studied are defined only on subsets unknown identifier 'X'X of ℝ : Typeℝ, and left undefined elsewhere. However, in Lean, this then creates some fiddly conversions when trying to restrict unknown identifier 'f'f to various subsets of unknown identifier 'X'X (which, technically, are not precisely subsets of ℝ : Typeℝ, though they can be coerced to such). To avoid this issue we will deviate from the text by having our functions defined on all of ℝ : Typeℝ (with the understanding that they are assigned "junk" values outside of the domain unknown identifier 'X'X of interest).

Визначення 9.3.1

abbrev Real.close_fn (ε:ℝ) (X:Set ℝ) (f: ℝ → ℝ) (L:ℝ) : Prop := ∀ x ∈ X, |f x - L| < ε

Визначення 9.3.3

abbrev Real.close_near (ε:ℝ) (X:Set ℝ) (f: ℝ → ℝ) (L:ℝ) (x₀:ℝ) : Prop := ∃ δ > 0, ε.close_fn (X ∩ Set.Ioo (x₀-δ) (x₀+δ)) f L
namespace Chapter9

Приклад 9.3.2

declaration uses 'sorry'example : (5:ℝ).close_fn (Set.Icc 1 3) (fun x ↦ x^2) 4 := ⊢ Real.close_fn 5 (Set.Icc 1 3) (fun x => x ^ 2) 4 All goals completed! 🐙

Приклад 9.3.2

declaration uses 'sorry'example : (0.41:ℝ).close_fn (Set.Icc 1.9 2.1) (fun x ↦ x^2) 4 := ⊢ Real.close_fn 0.41 (Set.Icc 1.9 2.1) (fun x => x ^ 2) 4 All goals completed! 🐙

Приклад 9.3.4

declaration uses 'sorry'example: ¬ (0.1:ℝ).close_fn (Set.Icc 1 3) (fun x ↦ x^2) 4 := ⊢ ¬Real.close_fn 0.1 (Set.Icc 1 3) (fun x => x ^ 2) 4 All goals completed! 🐙

Приклад 9.3.4

declaration uses 'sorry'example: (0.1:ℝ).close_near (Set.Icc 1 3) (fun x ↦ x^2) 4 2 := ⊢ Real.close_near 0.1 (Set.Icc 1 3) (fun x => x ^ 2) 4 2 All goals completed! 🐙

Приклад 9.3.5

declaration uses 'sorry'example: ¬ (0.1:ℝ).close_fn (Set.Icc 1 3) (fun x ↦ x^2) 9 := ⊢ ¬Real.close_fn 0.1 (Set.Icc 1 3) (fun x => x ^ 2) 9 All goals completed! 🐙

Приклад 9.3.5

declaration uses 'sorry'example: (0.1:ℝ).close_near (Set.Icc 1 3) (fun x ↦ x^2) 9 3 := ⊢ Real.close_near 0.1 (Set.Icc 1 3) (fun x => x ^ 2) 9 3 All goals completed! 🐙

Визначення 9.3.6 (Convergence of functions at a point)

abbrev Convergesto (X:Set ℝ) (f: ℝ → ℝ) (L:ℝ) (x₀:ℝ) : Prop := ∀ ε > (0:ℝ), ε.close_near X f L x₀

Connection with Mathlib filter convergence concepts

theorem Convergesto.iff (X:Set ℝ) (f: ℝ → ℝ) (L:ℝ) (x₀:ℝ) : Convergesto X f L x₀ ↔ Filter.Tendsto f ((nhds x₀) ⊓ Filter.principal X) (nhds L) := X:Set ℝf:ℝ → ℝL:ℝx₀:ℝ⊢ Convergesto X f L x₀ ↔ Filter.Tendsto f (nhds x₀ ⊓ Filter.principal X) (nhds L) X:Set ℝf:ℝ → ℝL:ℝx₀:ℝ⊢ (∀ ε > 0, ∃ δ > 0, ∀ x ∈ X ∩ Set.Ioo (x₀ - δ) (x₀ + δ), |f x - L| < ε) ↔ Filter.Tendsto f (nhds x₀ ⊓ Filter.principal X) (nhds L) X:Set ℝf:ℝ → ℝL:ℝx₀:ℝ⊢ (∀ ε > 0, ∃ δ > 0, ∀ x ∈ X ∩ Set.Ioo (x₀ - δ) (x₀ + δ), |f x - L| < ε) ↔ ∀ ε > 0, ∀ᶠ (b : ℝ) in nhds x₀ ⊓ Filter.principal X, |f b - L| < ε X:Set ℝf:ℝ → ℝL:ℝx₀:ℝ⊢ ∀ (a : ℝ), (a > 0 → ∃ δ > 0, ∀ x ∈ X ∩ Set.Ioo (x₀ - δ) (x₀ + δ), |f x - L| < a) ↔ a > 0 → ∀ᶠ (b : ℝ) in nhds x₀ ⊓ Filter.principal X, |f b - L| < a; X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝ⊢ (ε > 0 → ∃ δ > 0, ∀ x ∈ X ∩ Set.Ioo (x₀ - δ) (x₀ + δ), |f x - L| < ε) ↔ ε > 0 → ∀ᶠ (b : ℝ) in nhds x₀ ⊓ Filter.principal X, |f b - L| < ε X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝ⊢ ε > 0 → ((∃ δ > 0, ∀ x ∈ X ∩ Set.Ioo (x₀ - δ) (x₀ + δ), |f x - L| < ε) ↔ ∀ᶠ (b : ℝ) in nhds x₀ ⊓ Filter.principal X, |f b - L| < ε); X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0⊢ (∃ δ > 0, ∀ x ∈ X ∩ Set.Ioo (x₀ - δ) (x₀ + δ), |f x - L| < ε) ↔ ∀ᶠ (b : ℝ) in nhds x₀ ⊓ Filter.principal X, |f b - L| < ε X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0⊢ (∃ δ > 0, ∀ x ∈ X ∩ Set.Ioo (x₀ - δ) (x₀ + δ), |f x - L| < ε) ↔ ∀ᶠ (x : ℝ) in nhds x₀, x ∈ X → |f x - L| < ε X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0⊢ (∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε) ↔ ∃ l u, (l < x₀ ∧ x₀ < u) ∧ Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε} X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0⊢ (∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε) → ∃ l u, (l < x₀ ∧ x₀ < u) ∧ Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0⊢ (∃ l u, (l < x₀ ∧ x₀ < u) ∧ Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}) → ∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0⊢ (∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε) → ∃ l u, (l < x₀ ∧ x₀ < u) ∧ Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε} X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0δ:ℝhpos:0 < δhδ:∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε⊢ ∃ l u, (l < x₀ ∧ x₀ < u) ∧ Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε} use (x₀-δ), (x₀+δ), ⟨ X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0δ:ℝhpos:0 < δhδ:∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε⊢ x₀ - δ < x₀ All goals completed! 🐙, X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0δ:ℝhpos:0 < δhδ:∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε⊢ x₀ < x₀ + δ All goals completed! 🐙⟩ X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0δ:ℝhpos:0 < δhδ:∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < εx:ℝ⊢ x ∈ Set.Ioo (x₀ - δ) (x₀ + δ) → x ∈ {x | x ∈ X → |f x - L| < ε} X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0δ:ℝhpos:0 < δhδ:∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < εx:ℝ⊢ x₀ - δ < x → x < x₀ + δ → x ∈ X → |f x - L| < ε All goals completed! 🐙 X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:l < x₀h2:x₀ < u⊢ ∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε have h1' : 0 < x₀ - l := X:Set ℝf:ℝ → ℝL:ℝx₀:ℝ⊢ Convergesto X f L x₀ ↔ Filter.Tendsto f (nhds x₀ ⊓ Filter.principal X) (nhds L) All goals completed! 🐙 have h2' : 0 < u - x₀ := X:Set ℝf:ℝ → ℝL:ℝx₀:ℝ⊢ Convergesto X f L x₀ ↔ Filter.Tendsto f (nhds x₀ ⊓ Filter.principal X) (nhds L) All goals completed! 🐙 X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:l < x₀h2:x₀ < uh1':0 < x₀ - lh2':0 < u - x₀δ:ℝ := min (x₀ - l) (u - x₀)⊢ ∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:l < x₀h2:x₀ < uh1':0 < x₀ - lh2':0 < u - x₀δ:ℝ := min (x₀ - l) (u - x₀)hδ1:δ ≤ x₀ - l⊢ ∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:l < x₀h2:x₀ < uh1':0 < x₀ - lh2':0 < u - x₀δ:ℝ := min (x₀ - l) (u - x₀)hδ1:δ ≤ x₀ - lhδ2:δ ≤ u - x₀⊢ ∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε use δ, (X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:l < x₀h2:x₀ < uh1':0 < x₀ - lh2':0 < u - x₀δ:ℝ := min (x₀ - l) (u - x₀)hδ1:δ ≤ x₀ - lhδ2:δ ≤ u - x₀⊢ 0 < δ All goals completed! 🐙) X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:l < x₀h2:x₀ < uh1':0 < x₀ - lh2':0 < u - x₀δ:ℝ := min (x₀ - l) (u - x₀)hδ1:δ ≤ x₀ - lhδ2:δ ≤ u - x₀x:ℝhxX:x ∈ Xhx1:x₀ - δ < xhx2:x < x₀ + δ⊢ |f x - L| < ε have hmem : x ∈ Set.Ioo l u := X:Set ℝf:ℝ → ℝL:ℝx₀:ℝ⊢ Convergesto X f L x₀ ↔ Filter.Tendsto f (nhds x₀ ⊓ Filter.principal X) (nhds L) X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:l < x₀h2:x₀ < uh1':0 < x₀ - lh2':0 < u - x₀δ:ℝ := min (x₀ - l) (u - x₀)hδ1:δ ≤ x₀ - lhδ2:δ ≤ u - x₀x:ℝhxX:x ∈ Xhx1:x₀ - δ < xhx2:x < x₀ + δ⊢ l < x ∧ x < u exact ⟨ X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:l < x₀h2:x₀ < uh1':0 < x₀ - lh2':0 < u - x₀δ:ℝ := min (x₀ - l) (u - x₀)hδ1:δ ≤ x₀ - lhδ2:δ ≤ u - x₀x:ℝhxX:x ∈ Xhx1:x₀ - δ < xhx2:x < x₀ + δ⊢ l < x All goals completed! 🐙, X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:l < x₀h2:x₀ < uh1':0 < x₀ - lh2':0 < u - x₀δ:ℝ := min (x₀ - l) (u - x₀)hδ1:δ ≤ x₀ - lhδ2:δ ≤ u - x₀x:ℝhxX:x ∈ Xhx1:x₀ - δ < xhx2:x < x₀ + δ⊢ x < u All goals completed! 🐙 ⟩ X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝh1:l < x₀h2:x₀ < uh1':0 < x₀ - lh2':0 < u - x₀δ:ℝ := min (x₀ - l) (u - x₀)hδ1:δ ≤ x₀ - lhδ2:δ ≤ u - x₀x:ℝhxX:x ∈ Xhx1:x₀ - δ < xhx2:x < x₀ + δhmem:x ∈ Set.Ioo l uh:x ∈ {x | x ∈ X → |f x - L| < ε}⊢ |f x - L| < ε X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝh1:l < x₀h2:x₀ < uh1':0 < x₀ - lh2':0 < u - x₀δ:ℝ := min (x₀ - l) (u - x₀)hδ1:δ ≤ x₀ - lhδ2:δ ≤ u - x₀x:ℝhxX:x ∈ Xhx1:x₀ - δ < xhx2:x < x₀ + δhmem:x ∈ Set.Ioo l uh:|f x - L| < ε⊢ |f x - L| < ε; All goals completed! 🐙

Приклад 9.3.8

declaration uses 'sorry'example: Convergesto (Set.Icc 1 3) (fun x ↦ x^2) 4 2 := ⊢ Convergesto (Set.Icc 1 3) (fun x => x ^ 2) 4 2 All goals completed! 🐙

Твердження 9.3.9 / Вправа 9.3.1

theorem declaration uses 'sorry'Convergesto.iff_conv {E:Set ℝ} (f: ℝ → ℝ) (L:ℝ) {x₀:ℝ} (h: AdherentPt x₀ E) : Convergesto E f L x₀ ↔ ∀ a:ℕ → ℝ, (∀ n:ℕ, a n ∈ E) → Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n ↦ f (a n)) Filter.atTop (nhds L) := E:Set ℝf:ℝ → ℝL:ℝx₀:ℝh:AdherentPt x₀ E⊢ Convergesto E f L x₀ ↔ ∀ (a : ℕ → ℝ), (∀ (n : ℕ), a n ∈ E) → Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds L) All goals completed! 🐙
theorem Convergesto.comp {E:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (hf: Convergesto E f L x₀) {a:ℕ → ℝ} (ha: ∀ n:ℕ, a n ∈ E) (hconv: Filter.Tendsto a Filter.atTop (nhds x₀)) : Filter.Tendsto (fun n ↦ f (a n)) Filter.atTop (nhds L) := E:Set ℝf:ℝ → ℝL:ℝx₀:ℝh:AdherentPt x₀ Ehf:Convergesto E f L x₀a:ℕ → ℝha:∀ (n : ℕ), a n ∈ Ehconv:Filter.Tendsto a Filter.atTop (nhds x₀)⊢ Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds L) E:Set ℝf:ℝ → ℝL:ℝx₀:ℝh:AdherentPt x₀ Ehf:∀ (a : ℕ → ℝ), (∀ (n : ℕ), a n ∈ E) → Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds L)a:ℕ → ℝha:∀ (n : ℕ), a n ∈ Ehconv:Filter.Tendsto a Filter.atTop (nhds x₀)⊢ Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds L) All goals completed! 🐙
-- Ремарка 9.3.11 may possibly be inaccurate, in that one may be able to safely delete the hypothesis `AdherentPt x₀ E` in the above theorems. This is something that formalization might be able to clarify! If so, the hypothesis may also be deletable in several of the theorems below.

Наслідок 9.3.13

theorem Convergesto.uniq {E:Set ℝ} {f: ℝ → ℝ} {L L':ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (hf: Convergesto E f L x₀) (hf': Convergesto E f L' x₀) : L = L' := E:Set ℝf:ℝ → ℝL:ℝL':ℝx₀:ℝh:AdherentPt x₀ Ehf:Convergesto E f L x₀hf':Convergesto E f L' x₀⊢ L = L' -- цей доказ написан так, щоб співпадати із структурою орігінального тексту. E:Set ℝf:ℝ → ℝL:ℝL':ℝx₀:ℝh:AdherentPt x₀ Ehf:Convergesto E f L x₀hf':Convergesto E f L' x₀a:ℕ → ℝha:∀ (n : ℕ), a n ∈ Ehconv:Filter.Tendsto a Filter.atTop (nhds x₀)⊢ L = L' E:Set ℝf:ℝ → ℝL:ℝL':ℝx₀:ℝh:AdherentPt x₀ Ehf:Convergesto E f L x₀hf':Convergesto E f L' x₀a:ℕ → ℝha:∀ (n : ℕ), a n ∈ Ehconv:Filter.Tendsto a Filter.atTop (nhds x₀)hL:Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds L)⊢ L = L' E:Set ℝf:ℝ → ℝL:ℝL':ℝx₀:ℝh:AdherentPt x₀ Ehf:Convergesto E f L x₀hf':Convergesto E f L' x₀a:ℕ → ℝha:∀ (n : ℕ), a n ∈ Ehconv:Filter.Tendsto a Filter.atTop (nhds x₀)hL:Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds L)hL':Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds L')⊢ L = L' All goals completed! 🐙

Твердження 9.3.14 (Limit laws for functions)

theorem Convergesto.add {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (hf: Convergesto E f L x₀) (hg: Convergesto E g M x₀) : Convergesto E (f + g) (L + M) x₀ := E:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝh:AdherentPt x₀ Ehf:Convergesto E f L x₀hg:Convergesto E g M x₀⊢ Convergesto E (f + g) (L + M) x₀ -- цей доказ написан так, щоб співпадати із структурою орігінального тексту. E:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝh:AdherentPt x₀ Ehf:∀ (a : ℕ → ℝ), (∀ (n : ℕ), a n ∈ E) → Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds L)hg:∀ (a : ℕ → ℝ), (∀ (n : ℕ), a n ∈ E) → Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n => g (a n)) Filter.atTop (nhds M)⊢ ∀ (a : ℕ → ℝ), (∀ (n : ℕ), a n ∈ E) → Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n => (f + g) (a n)) Filter.atTop (nhds (L + M)) E:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝh:AdherentPt x₀ Ehf:∀ (a : ℕ → ℝ), (∀ (n : ℕ), a n ∈ E) → Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds L)hg:∀ (a : ℕ → ℝ), (∀ (n : ℕ), a n ∈ E) → Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n => g (a n)) Filter.atTop (nhds M)a:ℕ → ℝha:∀ (n : ℕ), a n ∈ Ehconv:Filter.Tendsto a Filter.atTop (nhds x₀)⊢ Filter.Tendsto (fun n => (f + g) (a n)) Filter.atTop (nhds (L + M)) E:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝh:AdherentPt x₀ Ehg:∀ (a : ℕ → ℝ), (∀ (n : ℕ), a n ∈ E) → Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n => g (a n)) Filter.atTop (nhds M)a:ℕ → ℝha:∀ (n : ℕ), a n ∈ Ehconv:Filter.Tendsto a Filter.atTop (nhds x₀)hf:Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds L)⊢ Filter.Tendsto (fun n => (f + g) (a n)) Filter.atTop (nhds (L + M)) E:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝh:AdherentPt x₀ Ea:ℕ → ℝha:∀ (n : ℕ), a n ∈ Ehconv:Filter.Tendsto a Filter.atTop (nhds x₀)hf:Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds L)hg:Filter.Tendsto (fun n => g (a n)) Filter.atTop (nhds M)⊢ Filter.Tendsto (fun n => (f + g) (a n)) Filter.atTop (nhds (L + M)) All goals completed! 🐙

Твердження 9.3.14 (Limit laws for functions) / Вправа 9.3.2

theorem declaration uses 'sorry'Convergesto.sub {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (hf: Convergesto E f L x₀) (hg: Convergesto E g M x₀) : Convergesto E (f - g) (L - M) x₀ := E:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝh:AdherentPt x₀ Ehf:Convergesto E f L x₀hg:Convergesto E g M x₀⊢ Convergesto E (f - g) (L - M) x₀ All goals completed! 🐙

Твердження 9.3.14 (Limit laws for functions) / Вправа 9.3.2

theorem declaration uses 'sorry'Convergesto.max {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (hf: Convergesto E f L x₀) (hg: Convergesto E g M x₀) : Convergesto E (max f g) (max L M) x₀ := E:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝh:AdherentPt x₀ Ehf:Convergesto E f L x₀hg:Convergesto E g M x₀⊢ Convergesto E (f ⊔ g) (Max.max L M) x₀ All goals completed! 🐙

Твердження 9.3.14 (Limit laws for functions) / Вправа 9.3.2

theorem declaration uses 'sorry'Convergesto.min {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (hf: Convergesto E f L x₀) (hg: Convergesto E g M x₀) : Convergesto E (min f g) (min L M) x₀ := E:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝh:AdherentPt x₀ Ehf:Convergesto E f L x₀hg:Convergesto E g M x₀⊢ Convergesto E (f ⊓ g) (Min.min L M) x₀ All goals completed! 🐙

Твердження 9.3.14 (Limit laws for functions) / Вправа 9.3.2

theorem declaration uses 'sorry'Convergesto.smul {E:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (hf: Convergesto E f L x₀) (c:ℝ) : Convergesto E (c • f) (c * L) x₀ := E:Set ℝf:ℝ → ℝL:ℝx₀:ℝh:AdherentPt x₀ Ehf:Convergesto E f L x₀c:ℝ⊢ Convergesto E (c • f) (c * L) x₀ All goals completed! 🐙

Твердження 9.3.14 (Limit laws for functions) / Вправа 9.3.2

theorem declaration uses 'sorry'Convergesto.mul {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (hf: Convergesto E f L x₀) (hg: Convergesto E g M x₀) : Convergesto E (f * g) (L * M) x₀ := E:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝh:AdherentPt x₀ Ehf:Convergesto E f L x₀hg:Convergesto E g M x₀⊢ Convergesto E (f * g) (L * M) x₀ All goals completed! 🐙

Твердження 9.3.14 (Limit laws for functions) / Вправа 9.3.2. The hypothesis in the book that g is non-vanishing on E can be dropped.

theorem declaration uses 'sorry'Convergesto.div {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (hM: M ≠ 0) (hf: Convergesto E f L x₀) (hg: Convergesto E g M x₀) : Convergesto E (f / g) (L / M) x₀ := E:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝh:AdherentPt x₀ EhM:M ≠ 0hf:Convergesto E f L x₀hg:Convergesto E g M x₀⊢ Convergesto E (f / g) (L / M) x₀ All goals completed! 🐙
theorem declaration uses 'sorry'Convergesto.const {E:Set ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (c:ℝ) : Convergesto E (fun x ↦ c) c x₀ := E:Set ℝx₀:ℝh:AdherentPt x₀ Ec:ℝ⊢ Convergesto E (fun x => c) c x₀ All goals completed! 🐙theorem declaration uses 'sorry'Convergesto.id {E:Set ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) : Convergesto E (fun x ↦ x) x₀ x₀ := E:Set ℝx₀:ℝh:AdherentPt x₀ E⊢ Convergesto E (fun x => x) x₀ x₀ All goals completed! 🐙theorem declaration uses 'sorry'Convergesto.sq {E:Set ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) : Convergesto E (fun x ↦ x^2) x₀ (x₀^2) := E:Set ℝx₀:ℝh:AdherentPt x₀ E⊢ Convergesto E (fun x => x ^ 2) x₀ (x₀ ^ 2) All goals completed! 🐙theorem declaration uses 'sorry'Convergesto.linear {E:Set ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (c:ℝ) : Convergesto E (fun x ↦ c * x) x₀ (c * x₀) := E:Set ℝx₀:ℝh:AdherentPt x₀ Ec:ℝ⊢ Convergesto E (fun x => c * x) x₀ (c * x₀) All goals completed! 🐙theorem declaration uses 'sorry'Convergesto.quadratic {E:Set ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (c d:ℝ) : Convergesto E (fun x ↦ x^2 + c * x + d) x₀ (x₀^2 + c * x₀ + d) := E:Set ℝx₀:ℝh:AdherentPt x₀ Ec:ℝd:ℝ⊢ Convergesto E (fun x => x ^ 2 + c * x + d) x₀ (x₀ ^ 2 + c * x₀ + d) All goals completed! 🐙theorem declaration uses 'sorry'Convergesto.restrict {X Y:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (h: AdherentPt x₀ X) (hf: Convergesto X f L x₀) (hY: Y ⊆ X) : Convergesto Y f L x₀ := X:Set ℝY:Set ℝf:ℝ → ℝL:ℝx₀:ℝh:AdherentPt x₀ Xhf:Convergesto X f L x₀hY:Y ⊆ X⊢ Convergesto Y f L x₀ All goals completed! 🐙theorem Real.sign_def (x:ℝ) : Real.sign x = if x < 0 then -1 else if x > 0 then 1 else 0 := rfl

Приклад 9.3.16

theorem declaration uses 'sorry'Convergesto.sign_right : Convergesto (Set.Ioi 0) Real.sign 1 0 := ⊢ Convergesto (Set.Ioi 0) Real.sign 1 0 All goals completed! 🐙

Приклад 9.3.16

theorem declaration uses 'sorry'Convergesto.sign_left : Convergesto (Set.Iio 0) Real.sign (-1) 0 := ⊢ Convergesto (Set.Iio 0) Real.sign (-1) 0 All goals completed! 🐙

Приклад 9.3.16

theorem declaration uses 'sorry'Convergesto.sign_all : ¬ ∃ L, Convergesto (Set.univ) Real.sign L 0 := ⊢ ¬∃ L, Convergesto Set.univ Real.sign L 0 All goals completed! 🐙
noncomputable abbrev f_9_3_17 : ℝ → ℝ := fun x ↦ if x = 0 then 1 else 0theorem declaration uses 'sorry'Convergesto.f_9_3_17_remove : Convergesto (Set.univ \ {0}) f_9_3_17 0 0 := ⊢ Convergesto (Set.univ \ {0}) f_9_3_17 0 0 All goals completed! 🐙theorem declaration uses 'sorry'Convergesto.f_9_3_17_all : ¬ ∃ L, Convergesto (Set.univ) f_9_3_17 L 0 := ⊢ ¬∃ L, Convergesto Set.univ f_9_3_17 L 0 All goals completed! 🐙

Твердження 9.3.18 / Вправа 9.3.3

theorem declaration uses 'sorry'Convergesto.local {E:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) {δ:ℝ} (hδ: δ > 0) : Convergesto E f L x₀ ↔ Convergesto (E ∩ Set.Ioo (x₀-δ) (x₀+δ)) f L x₀ := E:Set ℝf:ℝ → ℝL:ℝx₀:ℝh:AdherentPt x₀ Eδ:ℝhδ:δ > 0⊢ Convergesto E f L x₀ ↔ Convergesto (E ∩ Set.Ioo (x₀ - δ) (x₀ + δ)) f L x₀ All goals completed! 🐙

Приклад 9.3.19. The point of this example is somewhat blunted by the ability to remove the hypothesis that unknown identifier 'g'g is non-zero from the relevant part of Proposition 9.3.14

declaration uses 'sorry'example : Convergesto Set.univ (fun x ↦ (x+2)/(x+1)) (4/3:ℝ) 2 := ⊢ Convergesto Set.univ (fun x => (x + 2) / (x + 1)) (4 / 3) 2 All goals completed! 🐙

Приклад 9.3.20

declaration uses 'sorry'example : Convergesto (Set.univ \ {1}) (fun x ↦ (x^2-1)/(x-1)) 2 1 := ⊢ Convergesto (Set.univ \ {1}) (fun x => (x ^ 2 - 1) / (x - 1)) 2 1 All goals completed! 🐙
open Classical in /-- Приклад 9.3.21 -/ noncomputable abbrev f_9_3_21 : ℝ → ℝ := fun x ↦ if x ∈ (fun q:ℚ ↦ (q:ℝ)) '' Set.univ then 1 else 0declaration uses 'sorry'example : Filter.Tendsto (fun n ↦ f_9_3_21 (1/n:ℝ)) Filter.atTop (nhds 1) := ⊢ Filter.Tendsto (fun n => f_9_3_21 (1 / n)) Filter.atTop (nhds 1) All goals completed! 🐙declaration uses 'sorry'example : Filter.Tendsto (fun n ↦ f_9_3_21 ((Real.sqrt 2)/n:ℝ)) Filter.atTop (nhds 0) := ⊢ Filter.Tendsto (fun n => f_9_3_21 (√2 / n)) Filter.atTop (nhds 0) All goals completed! 🐙declaration uses 'sorry'example : ¬ ∃ L, Convergesto Set.univ f_9_3_21 L 0 := ⊢ ¬∃ L, Convergesto Set.univ f_9_3_21 L 0 All goals completed! 🐙
/- Вправа 9.3.4: State a definition of limit superior and limit inferior for functions, and prove an analogue of Proposition 9.3.9 for those definitions. -/

Вправа 9.3.5 (Continuous version of squeeze test)

theorem declaration uses 'sorry'Convergesto.squeeze {E:Set ℝ} {f g h: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (had: AdherentPt x₀ E) (hfg: ∀ x ∈ E, f x ≤ g x) (hgh: ∀ x ∈ E, g x ≤ h x) (hf: Convergesto E f L x₀) (hh: Convergesto E h L x₀) : Convergesto E g L x₀ := E:Set ℝf:ℝ → ℝg:ℝ → ℝh:ℝ → ℝL:ℝx₀:ℝhad:AdherentPt x₀ Ehfg:∀ x ∈ E, f x ≤ g xhgh:∀ x ∈ E, g x ≤ h xhf:Convergesto E f L x₀hh:Convergesto E h L x₀⊢ Convergesto E g L x₀ All goals completed! 🐙
end Chapter9