@[reducible, inline]

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

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

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₀ : ℝ} : 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₀ : ℝ} (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₀ : ℝ} (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, add)

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

Proposition 9.3.14 (Limit laws for functions, sub) / Exercise 9.3.2

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

Proposition 9.3.14 (Limit laws for functions, max) / Exercise 9.3.2

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

Proposition 9.3.14 (Limit laws for functions, min) / Exercise 9.3.2

theorem Chapter9.Convergesto.smul {E : Set ℝ} {f : ℝ → ℝ} {L x₀ : ℝ} (hf : Convergesto E f L x₀) (c : ℝ) : Convergesto E (c • f) (c * L) x₀

Proposition 9.3.14 (Limit laws for functions, smul) / Exercise 9.3.2

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

Proposition 9.3.14 (Limit laws for functions, mul) / Exercise 9.3.2

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

Proposition 9.3.14 (Limit laws for functions, div) / 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₀ c : ℝ) : Convergesto E (fun (x : ℝ) => c) c x₀

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

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

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

theorem Chapter9.Convergesto.quadratic (E : Set ℝ) (x₀ c d : ℝ) : Convergesto E (fun (x : ℝ) => x ^ 2 + c * x + d) (x₀ ^ 2 + c * x₀ + d) x₀

theorem Chapter9.Convergesto.restrict {X Y : Set ℝ} {f : ℝ → ℝ} {L 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 (a)

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

Example 9.3.16 (b)

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

Example 9.3.16 (c)

@[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δ : δ > 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₀ : ℝ} (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)