Analysis I, Section 9.9: Uniform continuity

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 UniformContinuousOn.
• Continuous functions on compact intervals 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₀)

Definition 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.CloseSeqs (ε : ℝ) (a b : Chapter6.Sequence) : Prop

Definition 9.9.5. This is similar but not identical to Real.close_seq from Section 6.1.

Equations

• ε.CloseSeqs a b = (a.m = b.m ∧ ∀ n ≥ a.m, ε.Close (a.seq n) (b.seq n))

@[reducible, inline]

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

Equations

• ε.EventuallyCloseSeqs a b = ∃ N ≥ a.m, ε.CloseSeqs (a.from N) (b.from N)

@[reducible, inline]

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

Equations

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

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

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

Lemma 9.9.7 / Exercise 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) → (↑x).equiv ↑y → (↑(f ∘ x)).equiv ↑(f ∘ y)

Proposition 9.9.8 / Exercise 9.9.2

theorem Chapter9.Chapter6.Sequence.equiv_const (x₀ : ℝ) (x : ℕ → ℝ) : Filter.Tendsto x Filter.atTop (nhds x₀) ↔ (↑x).equiv ↑fun (n : ℕ) => x₀

Remark 9.9.9

@[reducible, inline]

noncomputable abbrev Chapter9.f_9_9_10 : ℝ → ℝ

Example 9.9.10

Equations

• Chapter9.f_9_9_10 x = 1 / x

@[reducible, inline]

abbrev Chapter9.f_9_9_11 : ℝ → ℝ

Example 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 : (↑x).IsCauchy) (hmem : ∀ (n : ℕ), x n ∈ X) : (↑(f ∘ x)).IsCauchy

Proposition 9.9.12 / Exercise 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 (nhdsWithin x₀ X) (nhds L)

Corollary 9.9.14 / Exercise 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)

Proposition 9.9.15 / Exercise 9.9.5

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

Theorem 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

Exercise 9.9.6