Equicontinuity in metric spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This files contains various facts about (uniform) equicontinuity in metric spaces. Most importantly, we prove the usual characterization of equicontinuity of F at x₀ in the case of (pseudo) metric spaces: ∀ ε > 0, ∃ δ > 0, ∀ x, dist x x₀ < δ → ∀ i, dist (F i x₀) (F i x) < ε, and we prove that functions sharing a common (local or global) continuity modulus are (locally or uniformly) equicontinuous.

Main statements #

equicontinuous_at_iff: characterization of equicontinuity for families of functions between (pseudo) metric spaces.
equicontinuous_at_of_continuity_modulus: convenient way to prove equicontinuity at a point of a family of functions to a (pseudo) metric space by showing that they share a common local continuity modulus.
uniform_equicontinuous_of_continuity_modulus: convenient way to prove uniform equicontinuity of a family of functions to a (pseudo) metric space by showing that they share a common global continuity modulus.

Tags #

equicontinuity, continuity modulus

source

theorem metric.equicontinuous_at_iff_right {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] {ι : Type u_3} [topological_space β] {F : ι → β → α} {x₀ : β} :

equicontinuous_at F x₀ ↔ ∀ (ε : ℝ), ε > 0 → (∀ᶠ (x : β) in nhds x₀, ∀ (i : ι), has_dist.dist (F i x₀) (F i x) < ε)

Characterization of equicontinuity for families of functions taking values in a (pseudo) metric space.

source

theorem metric.equicontinuous_at_iff {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] {ι : Type u_3} [pseudo_metric_space β] {F : ι → β → α} {x₀ : β} :

equicontinuous_at F x₀ ↔ ∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ (x : β), has_dist.dist x x₀ < δ → ∀ (i : ι), has_dist.dist (F i x₀) (F i x) < ε)

Characterization of equicontinuity for families of functions between (pseudo) metric spaces.

source

@[protected]

theorem metric.equicontinuous_at_iff_pair {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] {ι : Type u_3} [topological_space β] {F : ι → β → α} {x₀ : β} :

equicontinuous_at F x₀ ↔ ∀ (ε : ℝ), ε > 0 → (∃ (U : set β) (H : U ∈ nhds x₀), ∀ (x : β), x ∈ U → ∀ (x' : β), x' ∈ U → ∀ (i : ι), has_dist.dist (F i x) (F i x') < ε)

Reformulation of equicontinuous_at_iff_pair for families of functions taking values in a (pseudo) metric space.

source

theorem metric.uniform_equicontinuous_iff_right {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] {ι : Type u_3} [uniform_space β] {F : ι → β → α} :

uniform_equicontinuous F ↔ ∀ (ε : ℝ), ε > 0 → (∀ᶠ (xy : β × β) in uniformity β, ∀ (i : ι), has_dist.dist (F i xy.fst) (F i xy.snd) < ε)

Characterization of uniform equicontinuity for families of functions taking values in a (pseudo) metric space.

source

theorem metric.uniform_equicontinuous_iff {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] {ι : Type u_3} [pseudo_metric_space β] {F : ι → β → α} :

uniform_equicontinuous F ↔ ∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ (x y : β), has_dist.dist x y < δ → ∀ (i : ι), has_dist.dist (F i x) (F i y) < ε)

Characterization of uniform equicontinuity for families of functions between (pseudo) metric spaces.

source

theorem metric.equicontinuous_at_of_continuity_modulus {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] {ι : Type u_3} [topological_space β] {x₀ : β} (b : β → ℝ) (b_lim : filter.tendsto b (nhds x₀) (nhds 0)) (F : ι → β → α) (H : ∀ᶠ (x : β) in nhds x₀, ∀ (i : ι), has_dist.dist (F i x₀) (F i x) ≤ b x) :

equicontinuous_at F x₀

For a family of functions to a (pseudo) metric spaces, a convenient way to prove equicontinuity at a point is to show that all of the functions share a common local continuity modulus.

source

theorem metric.uniform_equicontinuous_of_continuity_modulus {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] {ι : Type u_3} [pseudo_metric_space β] (b : ℝ → ℝ) (b_lim : filter.tendsto b (nhds 0) (nhds 0)) (F : ι → β → α) (H : ∀ (x y : β) (i : ι), has_dist.dist (F i x) (F i y) ≤ b (has_dist.dist x y)) :

uniform_equicontinuous F

For a family of functions between (pseudo) metric spaces, a convenient way to prove uniform equicontinuity is to show that all of the functions share a common global continuity modulus.

source

theorem metric.equicontinuous_of_continuity_modulus {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] {ι : Type u_3} [pseudo_metric_space β] (b : ℝ → ℝ) (b_lim : filter.tendsto b (nhds 0) (nhds 0)) (F : ι → β → α) (H : ∀ (x y : β) (i : ι), has_dist.dist (F i x) (F i y) ≤ b (has_dist.dist x y)) :

equicontinuous F

For a family of functions between (pseudo) metric spaces, a convenient way to prove equicontinuity is to show that all of the functions share a common global continuity modulus.