def book_uniformContinuous (S : Set ℝ) (f : ↑S → ℝ) : Prop

Definition 3.4.1. A function f : S → ℝ is uniformly continuous if for every ε > 0 there exists δ > 0 such that whenever x, c ∈ S with |x - c| < δ, then |f x - f c| < ε.

Equations

• book_uniformContinuous S f = ∀ ε > 0, ∃ δ > 0, ∀ (x c : ↑S), |↑x - ↑c| < δ → |f x - f c| < ε

theorem book_uniformContinuous_iff_uniformContinuous {S : Set ℝ} {f : ↑S → ℝ} : book_uniformContinuous S f ↔ UniformContinuous f

The book definition of uniform continuity on a subset of ℝ is equivalent to the standard UniformContinuous predicate for functions on the subtype.

theorem abs_sq_sub_sq_le_two_abs_sub {x y : { t : ℝ // t ∈ Set.Icc 0 1 }} : |↑x ^ 2 - ↑y ^ 2| ≤ 2 * |↑x - ↑y|

Helper lemma for Example 3.4.2: on [0, 1], the square function has Lipschitz constant 2.

theorem uniformContinuous_sq_on_Icc : UniformContinuous fun (x : { x : ℝ // x ∈ Set.Icc 0 1 }) => ↑x ^ 2

Example 3.4.2. The square function is uniformly continuous on the closed interval [0, 1], but it is not uniformly continuous on the whole real line.

theorem not_uniformContinuous_sq : ¬UniformContinuous fun (x : ℝ) => x ^ 2

Example 3.4.2. The square function ℝ → ℝ is not uniformly continuous on the entire real line.

theorem min_half_delta_mem_Ioo {δ : ℝ} (hδ : 0 < δ) : min (δ / 2) (1 / 3) ∈ Set.Ioo 0 1

Example 3.4.3 helper: the point min (δ/2) (1/3) lies in (0,1).

theorem inv_gap_for_double {t : ℝ} (ht : 0 < t) (hle : t ≤ 1 / 3) : |t⁻¹ - (2 * t)⁻¹| ≥ 3 / 2

theorem not_uniformContinuous_inv_on_Ioo : ¬UniformContinuous fun (x : { x : ℝ // x ∈ Set.Ioo 0 1 }) => (↑x)⁻¹

theorem uniformContinuousOn_Icc_of_continuous {a b : ℝ} {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc a b)) : UniformContinuousOn f (Set.Icc a b)

Theorem 3.4.4. If f : ℝ → ℝ is continuous on the closed interval [a, b], then f is uniformly continuous on [a, b].

theorem uniformContinuous.cauchySeq_image {S : Set ℝ} {f : ↑S → ℝ} (hf : UniformContinuous f) {x : ℕ → ↑S} (hx : CauchySeq x) : CauchySeq fun (n : ℕ) => f (x n)

Lemma 3.4.5. If f : S → ℝ is uniformly continuous and (x_n) is a Cauchy sequence in S, then (f x_n) is also Cauchy.

theorem uniformContinuousOn.cauchySeq_image {S : Set ℝ} {f : ℝ → ℝ} (hf : UniformContinuousOn f S) {x : ℕ → ℝ} (hx : ∀ (n : ℕ), x n ∈ S) (hxC : CauchySeq x) : CauchySeq fun (n : ℕ) => f (x n)

theorem cauchySeq_of_tendsto {x : ℕ → ℝ} {l : ℝ} (hx : Filter.Tendsto x Filter.atTop (nhds l)) : CauchySeq x

theorem denseInducing_subtype_Ioo_Icc {a b : ℝ} (h : a < b) : IsDenseInducing (Set.inclusion ⋯)

theorem uniformInducing_subtype_Ioo_Icc {a b : ℝ} : IsUniformInducing (Set.inclusion ⋯)

theorem uniformContinuousOn_extend_to_Icc {a b : ℝ} {f : ℝ → ℝ} (h : a < b) (hf : UniformContinuousOn f (Set.Ioo a b)) : ∃ (g : ℝ → ℝ), ContinuousOn g (Set.Icc a b) ∧ Set.EqOn g f (Set.Ioo a b) ∧ Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds (g a)) ∧ Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds (g b))

theorem uniformContinuousOn_Ioo_iff_limits_extend {a b : ℝ} (h : a < b) (f : ℝ → ℝ) : UniformContinuousOn f (Set.Ioo a b) ↔ ∃ (L_a : ℝ) (L_b : ℝ), Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds L_a) ∧ Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds L_b) ∧ ∃ (g : ℝ → ℝ), ContinuousOn g (Set.Icc a b) ∧ (∀ x ∈ Set.Ioo a b, g x = f x) ∧ g a = L_a ∧ g b = L_b

Proposition 3.4.6. Suppose a < b. A function f : (a, b) → ℝ is uniformly continuous if and only if the limits L_a = lim_{x → a} f x, L_b = lim_{x → b} f x exist and an extension to the closed interval sending a to L_a, b to L_b, and agreeing with f on (a, b) is continuous.

def book_lipschitzOn (S : Set ℝ) (f : ↑S → ℝ) : Prop

Definition 3.4.7. A function f : S → ℝ is Lipschitz continuous if there exists K ∈ ℝ such that |f x - f y| ≤ K * |x - y| for all x, y ∈ S.

Equations

• book_lipschitzOn S f = ∃ (K : ℝ), 0 ≤ K ∧ ∀ (x y : ↑S), |f x - f y| ≤ K * |↑x - ↑y|

theorem book_lipschitzOn_iff_lipschitzWith {S : Set ℝ} {f : ↑S → ℝ} : book_lipschitzOn S f ↔ ∃ (K : NNReal), LipschitzWith K f

The book definition of Lipschitz continuity on a subset of ℝ coincides with the existence of some ℝ≥0 Lipschitz constant for the subtype.

theorem uniformContinuous_of_book_lipschitzOn {S : Set ℝ} {f : ↑S → ℝ} (hf : book_lipschitzOn S f) : UniformContinuous f

Proposition 3.4.8. A Lipschitz continuous function is uniformly continuous.

theorem lipschitzWith_one_real_sin : LipschitzWith 1 fun (x : ℝ) => Real.sin x

Example 3.4.9. The sine function ℝ → ℝ is Lipschitz continuous with constant 1, as |sin x - sin y| ≤ |x - y| for all real x, y.

theorem lipschitzWith_one_real_cos : LipschitzWith 1 fun (x : ℝ) => Real.cos x

Example 3.4.9. The cosine function ℝ → ℝ is Lipschitz continuous with constant 1, since |cos x - cos y| ≤ |x - y| for all real x, y.

theorem sqrt_sub_le_sqrt_sub {x y : ℝ} (hx : 0 ≤ x) (hxy : x ≤ y) : √y - √x ≤ √(y - x)

theorem abs_sqrt_sub_le_sqrt_abs {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) : |√x - √y| ≤ √|x - y|

theorem book_lipschitzOn_sqrt_Ici_one : book_lipschitzOn (Set.Ici 1) fun (x : ↑(Set.Ici 1)) => √↑x

Example 3.4.10. The square root function f(x) = √x is Lipschitz continuous on [1, ∞) with constant 1/2, as |√x - √y| ≤ (1/2) |x - y| for x, y ≥ 1.

theorem not_book_lipschitzOn_sqrt_Ici_zero : ¬book_lipschitzOn (Set.Ici 0) fun (x : ↑(Set.Ici 0)) => √↑x

Example 3.4.10. The square root function g(x) = √x on [0, ∞) is not Lipschitz continuous; no global constant K can satisfy |√x - √y| ≤ K |x - y| on the whole domain.

theorem uniformContinuous_sqrt_Ici_zero : UniformContinuous fun (x : ↑(Set.Ici 0)) => √↑x

Example 3.4.10. Although not Lipschitz on [0, ∞), the square root function is uniformly continuous on that domain.