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

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:

• API for Mathlib's UniformContinousOn
• Continuous functions on compact intervls are uniformly continuous

theorem Chapter9.UniformContinuousOn.iff (f : ℝ → ℝ) (X : Set ℝ) : UniformContinuousOn f X ↔ ∀ ε > 0, ∃ δ > 0, ∀ x₀ ∈ X, ∀ x ∈ X, δ.close x x₀ → ε.close (f x) (f x₀)

Визначення 9.9.2. Here we use the Mathlib term UniformContinuousOn

theorem Chapter9.ContinuousOn.ofUniformContinuousOn {X : Set ℝ} (f : ℝ → ℝ) (hf : UniformContinuousOn f X) : ContinuousOn f X

@[reducible, inline]

abbrev Real.close_seqs (ε : ℝ) (a b : Chapter6.Sequence) : Prop

Визначення 9.9.5. This is similar but not identical to Real.close_seq from Section 6.1.

Equations

• ε.close_seqs a b = (a.m = b.m ∧ ∀ n ≥ a.m, ε.close (a.seq n) (b.seq n))

@[reducible, inline]

abbrev Real.eventually_close_seqs (ε : ℝ) (a b : Chapter6.Sequence) : Prop

Equations

• ε.eventually_close_seqs a b = ∃ N ≥ a.m, ε.close_seqs (a.from N) (b.from N)

@[reducible, inline]

abbrev Chapter6.Sequence.equiv (a b : Sequence) : Prop

Equations

• a.equiv b = ∀ ε > 0, ε.eventually_close_seqs a b

theorem Chapter6.Sequence.equiv_iff_rat (a b : Sequence) : a.equiv b ↔ ∀ ε > 0, (↑ε).eventually_close_seqs a b

Ремарка 9.9.6

theorem Chapter6.Sequence.equiv_iff (a b : Sequence) : a.equiv b ↔ Filter.Tendsto (fun (n : ℤ) => a.seq n - b.seq n) Filter.atTop (nhds 0)

Лема 9.9.7 / Вправа 9.9.1

theorem Chapter9.UniformContinuousOn.iff_preserves_equiv {X : Set ℝ} (f : ℝ → ℝ) : UniformContinuousOn f X ↔ ∀ (x y : ℕ → ℝ), (∀ (n : ℕ), x n ∈ X) → (∀ (n : ℕ), y n ∈ X) → { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then x n.toNat else 0, vanish := ⋯ }.equiv { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then y n.toNat else 0, vanish := ⋯ } → { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (f ∘ x) n.toNat else 0, vanish := ⋯ }.equiv { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (f ∘ y) n.toNat else 0, vanish := ⋯ }

Твердження 9.9.8 / Вправа 9.9.2

theorem Chapter9.Chapter6.Sequence.equiv_const (x₀ : ℝ) (x : ℕ → ℝ) : Filter.Tendsto x Filter.atTop (nhds x₀) ↔ { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then x n.toNat else 0, vanish := ⋯ }.equiv { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => x₀) n.toNat else 0, vanish := ⋯ }

Ремарка 9.9.9

@[reducible, inline]

noncomputable abbrev Chapter9.f_9_9_10 : ℝ → ℝ

Приклад 9.9.10

Equations

• Chapter9.f_9_9_10 x = 1 / x

@[reducible, inline]

abbrev Chapter9.f_9_9_11 : ℝ → ℝ

Приклад 9.9.11

Equations

• Chapter9.f_9_9_11 x = x ^ 2

theorem Chapter9.UniformContinuousOn.ofCauchy {X : Set ℝ} (f : ℝ → ℝ) (hf : UniformContinuousOn f X) {x : ℕ → ℝ} (hx : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then x n.toNat else 0, vanish := ⋯ }.isCauchy) (hmem : ∀ (n : ℕ), x n ∈ X) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (f ∘ x) n.toNat else 0, vanish := ⋯ }.isCauchy

Твердження 9.9.12 / Вправа 9.9.3

theorem Chapter9.UniformContinuousOn.limit_at_adherent {X : Set ℝ} (f : ℝ → ℝ) (hf : UniformContinuousOn f X) {x₀ : ℝ} (hx₀ : AdherentPt x₀ X) : ∃ (L : ℝ), Filter.Tendsto f (nhds x₀ ⊓ Filter.principal X) (nhds L)

Наслідок 9.9.14 / Вправа 9.9.4

theorem Chapter9.UniformContinuousOn.of_bounded {E X : Set ℝ} (f : ℝ → ℝ) (hf : UniformContinuousOn f X) (hEX : E ⊆ X) (hE : Bornology.IsBounded E) : Bornology.IsBounded (f '' E)

Твердження 9.9.15 / Вправа 9.9.5

theorem Chapter9.UniformContinuousOn.of_continuousOn {a b : ℝ} (hab : a < b) {f : ℝ → ℝ} (hcont : ContinuousOn f (Set.Icc a b)) : UniformContinuousOn f (Set.Icc a b)

Теорема 9.9.16

theorem Chapter9.UniformContinuousOn.comp {X Y : Set ℝ} {f g : ℝ → ℝ} (hf : UniformContinuousOn f X) (hg : UniformContinuousOn g Y) (hrange : f '' X ⊆ Y) : UniformContinuousOn (g ∘ f) X

Вправа 9.9.6