Аналіз 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:

• 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.close_fn (ε : ℝ) (X : Set ℝ) (f : ℝ → ℝ) (L : ℝ) : Prop

Визначення 9.3.1

Equations

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

@[reducible, inline]

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

Визначення 9.3.3

Equations

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

@[reducible, inline]

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

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

Equations

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

theorem Chapter9.Convergesto.iff (X : Set ℝ) (f : ℝ → ℝ) (L x₀ : ℝ) : Convergesto X f L x₀ ↔ Filter.Tendsto f (nhds x₀ ⊓ Filter.principal 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)

Твердження 9.3.9 / Вправа 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'

Наслідок 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₀

Твердження 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₀

Твердження 9.3.14 (Limit laws for functions) / Вправа 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₀

Твердження 9.3.14 (Limit laws for functions) / Вправа 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₀

Твердження 9.3.14 (Limit laws for functions) / Вправа 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₀

Твердження 9.3.14 (Limit laws for functions) / Вправа 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₀

Твердження 9.3.14 (Limit laws for functions) / Вправа 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₀

Твердження 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 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

Приклад 9.3.16

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

Приклад 9.3.16

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

Приклад 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₀

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

@[reducible, inline]

noncomputable abbrev Chapter9.f_9_3_21 : ℝ → ℝ

Приклад 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₀

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