1. Analysis
  2. 9.3. Limiting values of functions
Imports
import Mathlib.Tactic import Mathlib.Data.Real.Sign import Analysis.Section_9_1
set_option doc.verso.suggestions false

Analysis I, Section 9.3: Limiting values of functions

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:

  • Limits of continuous functions

  • Connection with Mathilb's filter convergence concepts

  • Limit laws for functions

Technical point: in the text, the functions f studied are defined only on subsets X of ℝ, and left undefined elsewhere. However, in Lean, this then creates some fiddly conversions when trying to restrict f to various subsets of X (which, technically, are not precisely subsets of ℝ, 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 ℝ (with the understanding that they are assigned "junk" values outside of the domain X of interest).

Definition 9.3.1 Note the books uses ≤ instead of <, but < matches mathlib's definition of neighborhood.

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

Definition 9.3.3

abbrev Real.CloseNear (ε:ℝ) (X:Set ℝ) (f: ℝ → ℝ) (L:ℝ) (x₀:ℝ) : Prop := ∃ δ > 0, ε.CloseFn (X ∩ .Ioo (x₀-δ) (x₀+δ)) f L
namespace Chapter9/-- Example 9.3.2 Slight change from the book to accomodate the change to {lean}`Real.CloseFn` -/ declaration uses `sorry`example : (5.1:ℝ).CloseFn (.Icc 1 3) (fun x ↦ x^2) 4 := ⊢ Real.CloseFn 5.1 (Set.Icc 1 3) (fun x ↦ x ^ 2) 4 All goals completed! 🐙/-- Example 9.3.2 Slight change from the book to accomodate the change to {lean}`Real.CloseFn` -/ declaration uses `sorry`example : (0.42:ℝ).CloseFn (.Icc 1.9 2.1) (fun x ↦ x^2) 4 := ⊢ Real.CloseFn 0.42 (Set.Icc 1.9 2.1) (fun x ↦ x ^ 2) 4 All goals completed! 🐙/-- Example 9.3.4 -/ declaration uses `sorry`example: ¬(0.1:ℝ).CloseFn (.Icc 1 3) (fun x ↦ x^2) 4 := ⊢ ¬Real.CloseFn 0.1 (Set.Icc 1 3) (fun x ↦ x ^ 2) 4 All goals completed! 🐙/-- Example 9.3.4 -/ declaration uses `sorry`example: (0.1:ℝ).CloseNear (.Icc 1 3) (fun x ↦ x^2) 4 2 := ⊢ Real.CloseNear 0.1 (Set.Icc 1 3) (fun x ↦ x ^ 2) 4 2 All goals completed! 🐙/-- Example 9.3.5 -/ declaration uses `sorry`example: ¬(0.1:ℝ).CloseFn (.Icc 1 3) (fun x ↦ x^2) 9 := ⊢ ¬Real.CloseFn 0.1 (Set.Icc 1 3) (fun x ↦ x ^ 2) 9 All goals completed! 🐙/-- Example 9.3.5 -/ declaration uses `sorry`example: (0.1:ℝ).CloseNear (.Icc 1 3) (fun x ↦ x^2) 9 3 := ⊢ Real.CloseNear 0.1 (Set.Icc 1 3) (fun x ↦ x ^ 2) 9 3 All goals completed! 🐙

Definition 9.3.6 (Convergence of functions at a point)

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

Connection with Mathlib filter convergence concepts

theorem Convergesto.iff (X:Set ℝ) (f: ℝ → ℝ) (L:ℝ) (x₀:ℝ) : Convergesto X f L x₀ ↔ (nhdsWithin x₀ X).Tendsto f (nhds L) := X:Set ℝf:ℝ → ℝL:ℝx₀:ℝ⊢ Convergesto X f L x₀ ↔ Filter.Tendsto f (nhdsWithin x₀ 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₀:ℝε:ℝ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δ:ℝleft✝:0 < δright✝:∀ 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δ:ℝleft✝:0 < δright✝:∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε⊢ x₀ - δ < x₀ ∧ x₀ < x₀ + δ All goals completed! 🐙 X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0δ:ℝleft✝:0 < δright✝:∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < εa✝:ℝ⊢ a✝ ∈ Set.Ioo (x₀ - δ) (x₀ + δ) → a✝ ∈ {x | x ∈ X → |f x - L| < ε}; X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0δ:ℝleft✝:0 < δright✝:∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < εa✝:ℝ⊢ x₀ - δ < a✝ → a✝ < x₀ + δ → a✝ ∈ X → |f a✝ - L| < ε; All goals completed! 🐙 X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝleft✝:l < x₀right✝:x₀ < uh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}⊢ ∃ δ, 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 (nhdsWithin x₀ X) (nhds L) All goals completed! 🐙 have h2 : 0 < u - x₀ := X:Set ℝf:ℝ → ℝL:ℝx₀:ℝ⊢ Convergesto X f L x₀ ↔ Filter.Tendsto f (nhdsWithin x₀ X) (nhds L) All goals completed! 🐙 X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝleft✝:l < x₀right✝:x₀ < uh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1: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:ℝleft✝:l < x₀right✝:x₀ < uh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:0 < x₀ - lh2:0 < u - x₀δ:ℝ := min (x₀ - l) (u - x₀)hδ1:min (x₀ - l) (u - x₀) ≤ x₀ - l⊢ ∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝleft✝:l < x₀right✝:x₀ < uh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:0 < x₀ - lh2:0 < u - x₀δ:ℝ := min (x₀ - l) (u - x₀)hδ1:min (x₀ - l) (u - x₀) ≤ x₀ - lhδ2:min (x₀ - l) (u - x₀) ≤ u - x₀⊢ ∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε use δ, (X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝleft✝:l < x₀right✝:x₀ < uh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:0 < x₀ - lh2:0 < u - x₀δ:ℝ := min (x₀ - l) (u - x₀)hδ1:min (x₀ - l) (u - x₀) ≤ x₀ - lhδ2:min (x₀ - l) (u - x₀) ≤ u - x₀⊢ 0 < δ All goals completed! 🐙); intro x X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝleft✝:l < x₀right✝:x₀ < uh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:0 < x₀ - lh2:0 < u - x₀δ:ℝ := min (x₀ - l) (u - x₀)hδ1:min (x₀ - l) (u - x₀) ≤ x₀ - lhδ2:min (x₀ - l) (u - x₀) ≤ u - x₀x:ℝhxX:x ∈ X⊢ x₀ - δ < x → x < x₀ + δ → |f x - L| < ε X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝleft✝:l < x₀right✝:x₀ < uh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:0 < x₀ - lh2:0 < u - x₀δ:ℝ := min (x₀ - l) (u - x₀)hδ1:min (x₀ - l) (u - x₀) ≤ x₀ - lhδ2:min (x₀ - l) (u - x₀) ≤ u - x₀x:ℝhxX:x ∈ Xa✝:x₀ - δ < x⊢ x < x₀ + δ → |f x - L| < ε X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝleft✝:l < x₀right✝:x₀ < uh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:0 < x₀ - lh2:0 < u - x₀δ:ℝ := min (x₀ - l) (u - x₀)hδ1:min (x₀ - l) (u - x₀) ≤ x₀ - lhδ2:min (x₀ - l) (u - x₀) ≤ u - x₀x:ℝhxX:x ∈ Xa✝¹:x₀ - δ < xa✝:x < x₀ + δ⊢ |f x - L| < ε specialize h (show x ∈ .Ioo l u X:Set ℝf:ℝ → ℝL:ℝx₀:ℝ⊢ Convergesto X f L x₀ ↔ Filter.Tendsto f (nhdsWithin x₀ X) (nhds L) X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝleft✝:l < x₀right✝:x₀ < uh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:0 < x₀ - lh2:0 < u - x₀δ:ℝ := min (x₀ - l) (u - x₀)hδ1:min (x₀ - l) (u - x₀) ≤ x₀ - lhδ2:min (x₀ - l) (u - x₀) ≤ u - x₀x:ℝhxX:x ∈ Xa✝¹:x₀ - δ < xa✝:x < x₀ + δ⊢ l < x ∧ x < u; All goals completed! 🐙) All goals completed! 🐙
/-- Example 9.3.8 -/ declaration uses `sorry`example: Convergesto (.Icc 1 3) (fun x ↦ x^2) 4 2 := ⊢ Convergesto (Set.Icc 1 3) (fun x ↦ x ^ 2) 4 2 All goals completed! 🐙

Proposition 9.3.9 / Exercise 9.3.1

theorem declaration uses `sorry`Convergesto.iff_conv {E:Set ℝ} (f: ℝ → ℝ) (L:ℝ) {x₀:ℝ} : Convergesto E f L x₀ ↔ ∀ a:ℕ → ℝ, (∀ n:ℕ, a n ∈ E) → Filter.atTop.Tendsto a (nhds x₀) → Filter.atTop.Tendsto (fun n ↦ f (a n)) (nhds L) := E:Set ℝf:ℝ → ℝL:ℝx₀:ℝ⊢ 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₀:ℝ} (hf: Convergesto E f L x₀) {a:ℕ → ℝ} (ha: ∀ n:ℕ, a n ∈ E) (hconv: Filter.atTop.Tendsto a (nhds x₀)) : Filter.atTop.Tendsto (fun n ↦ f (a n)) (nhds L) := E:Set ℝf:ℝ → ℝL:ℝx₀:ℝhf: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₀:ℝhf:∀ (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! 🐙

Corollary 9.3.13

-- Remark 9.3.11 is not quite true in Lean: the hypothesis `AdherentPt x₀ E` is safely removed -- from most theorems (with the exception of Convergesto.uniq). 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' -- This proof is written to follow the structure of the original text. 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' All goals completed! 🐙

Proposition 9.3.14 (Limit laws for functions)

theorem Convergesto.add {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (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₀:ℝhf:Convergesto E f L x₀hg:Convergesto E g M x₀⊢ Convergesto E (f + g) (L + M) x₀ -- This proof is written to follow the structure of the original text. E:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝhf:∀ (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)) intro a E:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝhf:∀ (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 ∈ 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₀:ℝhf:∀ (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₀:ℝ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₀)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₀:ℝ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)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! 🐙

Proposition 9.3.14 (Limit laws for functions) / Exercise 9.3.2

theorem declaration uses `sorry`Convergesto.sub {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (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₀:ℝhf:Convergesto E f L x₀hg:Convergesto E g M x₀⊢ Convergesto E (f - g) (L - M) x₀ All goals completed! 🐙

Proposition 9.3.14 (Limit laws for functions) / Exercise 9.3.2

theorem declaration uses `sorry`Convergesto.max {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (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₀:ℝhf:Convergesto E f L x₀hg:Convergesto E g M x₀⊢ Convergesto E (f ⊔ g) (Max.max L M) x₀ All goals completed! 🐙

Proposition 9.3.14 (Limit laws for functions) / Exercise 9.3.2

theorem declaration uses `sorry`Convergesto.min {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (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₀:ℝhf:Convergesto E f L x₀hg:Convergesto E g M x₀⊢ Convergesto E (f ⊓ g) (Min.min L M) x₀ All goals completed! 🐙

Proposition 9.3.14 (Limit laws for functions) / Exercise 9.3.2

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

Proposition 9.3.14 (Limit laws for functions) / Exercise 9.3.2

theorem declaration uses `sorry`Convergesto.mul {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (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₀:ℝhf:Convergesto E f L x₀hg:Convergesto E g M x₀⊢ Convergesto E (f * g) (L * M) x₀ All goals completed! 🐙

Proposition 9.3.14 (Limit laws for functions) / Exercise 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₀:ℝ} (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₀:ℝhM: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₀:ℝ) (c:ℝ) : Convergesto E (fun _ ↦ c) c x₀ := E:Set ℝx₀:ℝc:ℝ⊢ Convergesto E (fun x ↦ c) c x₀ All goals completed! 🐙theorem declaration uses `sorry`Convergesto.id (E:Set ℝ) (x₀:ℝ) : Convergesto E (fun x ↦ x) x₀ x₀ := E:Set ℝx₀:ℝ⊢ Convergesto E (fun x ↦ x) x₀ x₀ All goals completed! 🐙theorem declaration uses `sorry`Convergesto.sq (E:Set ℝ) (x₀:ℝ) : Convergesto E (fun x ↦ x^2) (x₀^2) x₀ := E:Set ℝx₀:ℝ⊢ Convergesto E (fun x ↦ x ^ 2) (x₀ ^ 2) x₀ All goals completed! 🐙theorem declaration uses `sorry`Convergesto.linear (E:Set ℝ) (x₀:ℝ) (c:ℝ) : Convergesto E (fun x ↦ c * x) (c * x₀) x₀ := E:Set ℝx₀:ℝc:ℝ⊢ Convergesto E (fun x ↦ c * x) (c * x₀) x₀ All goals completed! 🐙theorem declaration uses `sorry`Convergesto.quadratic (E:Set ℝ) (x₀:ℝ) (c d:ℝ) : Convergesto E (fun x ↦ x^2 + c * x + d) (x₀^2 + c * x₀ + d) x₀ := E:Set ℝx₀:ℝc:ℝd:ℝ⊢ Convergesto E (fun x ↦ x ^ 2 + c * x + d) (x₀ ^ 2 + c * x₀ + d) x₀ All goals completed! 🐙theorem declaration uses `sorry`Convergesto.restrict {X Y:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (hf: Convergesto X f L x₀) (hY: Y ⊆ X) : Convergesto Y f L x₀ := X:Set ℝY:Set ℝf:ℝ → ℝL:ℝx₀:ℝhf: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

Example 9.3.16

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

Example 9.3.16

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

Example 9.3.16

theorem declaration uses `sorry`Convergesto.sign_all : ¬ ∃ L, Convergesto (.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 (.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 .univ f_9_3_17 L 0 := ⊢ ¬∃ L, Convergesto Set.univ f_9_3_17 L 0 All goals completed! 🐙

Proposition 9.3.18 / Exercise 9.3.3

theorem declaration uses `sorry`Convergesto.local {E:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ} {δ:ℝ} (hδ: δ > 0) : Convergesto E f L x₀ ↔ Convergesto (E ∩ .Ioo (x₀-δ) (x₀+δ)) f L x₀ := E:Set ℝf:ℝ → ℝL:ℝx₀:ℝδ:ℝhδ:δ > 0⊢ Convergesto E f L x₀ ↔ Convergesto (E ∩ Set.Ioo (x₀ - δ) (x₀ + δ)) f L x₀ All goals completed! 🐙
/-- Example 9.3.19. The point of this example is somewhat blunted by the ability to remove the hypothesis that {lit}`g` is non-zero from the relevant part of Proposition 9.3.14 -/ declaration uses `sorry`example : Convergesto .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! 🐙/-- Example 9.3.20 -/ declaration uses `sorry`example : Convergesto (.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! 🐙

Example 9.3.21

open Classical innoncomputable abbrev f_9_3_21 : ℝ → ℝ := fun x ↦ if x ∈ (fun q:ℚ ↦ (q:ℝ)) '' .univ then 1 else 0
declaration uses `sorry`example : Filter.atTop.Tendsto (fun n ↦ f_9_3_21 (1/n:ℝ)) (nhds 1) := ⊢ Filter.Tendsto (fun n ↦ f_9_3_21 (1 / n)) Filter.atTop (nhds 1) All goals completed! 🐙declaration uses `sorry`example : Filter.atTop.Tendsto (fun n ↦ f_9_3_21 ((Real.sqrt 2)/n:ℝ)) (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 .univ f_9_3_21 L 0 := ⊢ ¬∃ L, Convergesto Set.univ f_9_3_21 L 0 All goals completed! 🐙

Exercise 9.3.5 (Continuous version of squeeze test)

/- Exercise 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. -/ theorem declaration uses `sorry`Convergesto.squeeze {E:Set ℝ} {f g h: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (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₀:ℝhfg:∀ 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