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).

@[reducible, inline]

abbrev Real.CloseFn (ε : ℝ) (X : Set ℝ) (f : ℝ → ℝ) (L : ℝ) : Prop

Definition 9.3.1

Equations

• ε.CloseFn X f L = ∀ x ∈ X, |f x - L| < ε

@[reducible, inline]

abbrev Real.CloseNear (ε : ℝ) (X : Set ℝ) (f : ℝ → ℝ) (L x₀ : ℝ) : Prop

Definition 9.3.3

Equations

• ε.CloseNear X f L x₀ = ∃ δ > 0, ε.CloseFn (X ∩ Set.Ioo (x₀ - δ) (x₀ + δ)) f L

@[reducible, inline]

abbrev Chapter9.Convergesto (X : Set ℝ) (f : ℝ → ℝ) (L x₀ : ℝ) : Prop

Definition 9.3.6 (Convergence of functions at a point)

Equations

• Chapter9.Convergesto X f L x₀ = ∀ ε > 0, ε.CloseNear X f L x₀

theorem Chapter9.Convergesto.iff (X : Set ℝ) (f : ℝ → ℝ) (L x₀ : ℝ) : Convergesto X f L x₀ ↔ Filter.Tendsto f (nhdsWithin x₀ X) (nhds L)

Connection with Mathlib filter convergence concepts

theorem Chapter9.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)

Proposition 9.3.9 / Exercise 9.3.1

theorem Chapter9.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)

theorem Chapter9.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'

Corollary 9.3.13

theorem Chapter9.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₀

Proposition 9.3.14 (Limit laws for functions)

theorem Chapter9.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₀

Proposition 9.3.14 (Limit laws for functions) / Exercise 9.3.2

theorem Chapter9.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 (f ⊔ g) (Max.max L M) x₀

Proposition 9.3.14 (Limit laws for functions) / Exercise 9.3.2

theorem Chapter9.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 (f ⊓ g) (Min.min L M) x₀

Proposition 9.3.14 (Limit laws for functions) / Exercise 9.3.2

theorem Chapter9.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₀

Proposition 9.3.14 (Limit laws for functions) / Exercise 9.3.2

theorem Chapter9.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₀

Proposition 9.3.14 (Limit laws for functions) / Exercise 9.3.2

theorem Chapter9.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₀

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 Chapter9.Convergesto.const {E : Set ℝ} {x₀ : ℝ} (h : AdherentPt x₀ E) (c : ℝ) : Convergesto E (fun (x : ℝ) => c) c x₀

theorem Chapter9.Convergesto.id {E : Set ℝ} {x₀ : ℝ} (h : AdherentPt x₀ E) : Convergesto E (fun (x : ℝ) => x) x₀ x₀

theorem Chapter9.Convergesto.sq {E : Set ℝ} {x₀ : ℝ} (h : AdherentPt x₀ E) : Convergesto E (fun (x : ℝ) => x ^ 2) x₀ (x₀ ^ 2)

theorem Chapter9.Convergesto.linear {E : Set ℝ} {x₀ : ℝ} (h : AdherentPt x₀ E) (c : ℝ) : Convergesto E (fun (x : ℝ) => c * x) x₀ (c * x₀)

theorem Chapter9.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)

theorem Chapter9.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₀

theorem Chapter9.Real.sign_def (x : ℝ) : x.sign = if x < 0 then -1 else if x > 0 then 1 else 0

theorem Chapter9.Convergesto.sign_right : Convergesto (Set.Ioi 0) Real.sign 1 0

Example 9.3.16

theorem Chapter9.Convergesto.sign_left : Convergesto (Set.Iio 0) Real.sign (-1) 0

Example 9.3.16

theorem Chapter9.Convergesto.sign_all : ¬∃ (L : ℝ), Convergesto Set.univ Real.sign L 0

Example 9.3.16

@[reducible, inline]

noncomputable abbrev Chapter9.f_9_3_17 : ℝ → ℝ

Equations

• Chapter9.f_9_3_17 x = if x = 0 then 1 else 0

theorem Chapter9.Convergesto.f_9_3_17_remove : Convergesto (Set.univ \ {0}) f_9_3_17 0 0

theorem Chapter9.Convergesto.f_9_3_17_all : ¬∃ (L : ℝ), Convergesto Set.univ f_9_3_17 L 0

theorem Chapter9.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₀

Proposition 9.3.18 / Exercise 9.3.3

@[reducible, inline]

noncomputable abbrev Chapter9.f_9_3_21 : ℝ → ℝ

Example 9.3.21

Equations

• Chapter9.f_9_3_21 x = if x ∈ (fun (q : ℚ) => ↑q) '' Set.univ then 1 else 0

theorem Chapter9.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₀

Exercise 9.3.5 (Continuous version of squeeze test)