Equicontinuity in metric spaces

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

• Metric.equicontinuousAt_iff: characterization of equicontinuity for families of functions between (pseudo) metric spaces.
• Metric.equicontinuousAt_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.
• Metric.uniformEquicontinuous_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

theorem Metric.equicontinuousAt_iff_right {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] {ι : Type u_4} [TopologicalSpace β] {F : ι → β → α} {x₀ : β} : EquicontinuousAt F x₀ ↔ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : β) in nhds x₀, ∀ (i : ι), dist (F i x₀) (F i x) < ε

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

theorem Metric.equicontinuousAt_iff {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] {ι : Type u_4} [PseudoMetricSpace β] {F : ι → β → α} {x₀ : β} : EquicontinuousAt F x₀ ↔ ∀ (ε : ℝ), ε > 0 → ∃ δ, δ > 0 ∧ ∀ (x : β), dist x x₀ < δ → ∀ (i : ι), dist (F i x₀) (F i x) < ε

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

theorem Metric.equicontinuousAt_iff_pair {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] {ι : Type u_4} [TopologicalSpace β] {F : ι → β → α} {x₀ : β} : EquicontinuousAt F x₀ ↔ ∀ (ε : ℝ), ε > 0 → ∃ U, U ∈ nhds x₀ ∧ ∀ (x : β), x ∈ U → ∀ (x' : β), x' ∈ U → ∀ (i : ι), dist (F i x) (F i x') < ε

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

theorem Metric.uniformEquicontinuous_iff_right {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] {ι : Type u_4} [UniformSpace β] {F : ι → β → α} : UniformEquicontinuous F ↔ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (xy : β × β) in uniformity β, ∀ (i : ι), dist (F i xy.fst) (F i xy.snd) < ε

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

theorem Metric.uniformEquicontinuous_iff {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] {ι : Type u_4} [PseudoMetricSpace β] {F : ι → β → α} : UniformEquicontinuous F ↔ ∀ (ε : ℝ), ε > 0 → ∃ δ, δ > 0 ∧ ∀ (x y : β), dist x y < δ → ∀ (i : ι), dist (F i x) (F i y) < ε

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

theorem Metric.equicontinuousAt_of_continuity_modulus {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] {ι : Type u_4} [TopologicalSpace β] {x₀ : β} (b : β → ℝ) (b_lim : Filter.Tendsto b (nhds x₀) (nhds 0)) (F : ι → β → α) (H : ∀ᶠ (x : β) in nhds x₀, ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x) : EquicontinuousAt 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.

theorem Metric.uniformEquicontinuous_of_continuity_modulus {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] {ι : Type u_4} [PseudoMetricSpace β] (b : ℝ → ℝ) (b_lim : Filter.Tendsto b (nhds 0) (nhds 0)) (F : ι → β → α) (H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)) : UniformEquicontinuous 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.

theorem Metric.equicontinuous_of_continuity_modulus {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] {ι : Type u_4} [PseudoMetricSpace β] (b : ℝ → ℝ) (b_lim : Filter.Tendsto b (nhds 0) (nhds 0)) (F : ι → β → α) (H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (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.