The Arzelà–Ascoli theorem in C(X, Y)

Mathlib proves the Arzelà–Ascoli theorem for a family of functions viewed inside a space of uniform convergence on a family of compact sets (ArzelaAscoli.isCompact_closure_of_isClosedEmbedding), and shows that an equicontinuous set of continuous maps that is compact for pointwise convergence is compact (ArzelaAscoli.isCompact_of_equicontinuous). This file states it directly for subsets of the space C(X, Y) of continuous maps with its compact-open topology, which is the space of continuous curves when X is a compact interval, and adds companion statements used for compactness and finite approximation of families of curves.

• An equicontinuous family in C(X, Y) whose values at each point lie in a common compact set has relatively compact range.
• If Y is complete, it is enough that the values are totally bounded at the points of a dense set D ⊆ X: equicontinuity spreads total boundedness from D to every point (EquicontinuousWithinAt.totallyBounded_range_eval), and completeness turns it into compactness of the closure.
• An equicontinuous family with pointwise totally bounded values has finite uniform approximations on compact sets, with approximants drawn from the family itself.
• Conversely, on a weakly locally compact domain, a compact subset of C(X, Y) is equicontinuous.
• A sequence of continuous 1-periodic loops in a compact subset of a pseudometric space, with a common modulus of continuity on [0, 1], has a subsequence converging uniformly on ℝ. In particular the 1-periodic L-Lipschitz loops in a compact set form a compact subset of ℝ →ᵤ M.
• The translates (s, t) ↦ u(s + σₙ, t), σₙ → ∞, of a Lipschitz map on a half-plane s ≥ b with values in a compact set have a subsequence converging locally uniformly on the plane.
• The C-Lipschitz paths I → Y starting at a point x form a compact subset of C(I, Y) when the closed ball of radius C about x is compact, in particular when Y is proper.

The pointwise hypothesis cannot be replaced by equicontinuity and a common starting point when Y is not proper. The curves γₙ(t) = t • eₙ, t ∈ [0, 1], along the standard basis vectors of ℓ² are 1-Lipschitz and all start at 0, but no subsequence converges uniformly, because the endpoints eₙ stay at distance at least 1 from each other (TauCeti.exists_lipschitzWith_one_not_isCompact_closure_range).

Main results

• ArzelaAscoli.isCompact_closure_range_of_equicontinuous: equicontinuity and pointwise relative compactness give compact closure.
• EquicontinuousOn.exists_finite_approx_of_isCompact: finite uniform approximation on a compact set by members of the family.
• ContinuousMap.isClosedEmbedding_toUniformOnFunIsCompact: C(X, Y) is a closed subspace of the space of functions with the topology of uniform convergence on compacts.
• ArzelaAscoli.isCompact_closure_of_equicontinuous_of_totallyBounded: for a complete target, total boundedness of the values at the points of a dense set suffices.
• IsCompact.equicontinuous: a compact set of continuous maps on a weakly locally compact space is equicontinuous.
• TauCeti.exists_tendstoUniformly_subseq_of_periodic_of_modulus: Arzelà–Ascoli for periodic loops with a common modulus of continuity.
• TauCeti.isCompact_setOf_periodic_lipschitzWith: the 1-periodic L-Lipschitz loops in a compact set are compact for uniform convergence on ℝ.
• TauCeti.exists_subseq_tendstoLocallyUniformly_comp_add: translates u(s + σₙ, t), σₙ → ∞, of a Lipschitz map on a half-plane s ≥ b with values in a compact set have a locally uniformly convergent subsequence.
• TauCeti.isCompact_setOf_lipschitzWith_apply_zero_eq: in a proper space, uniformly Lipschitz paths with a common starting point form a compact set, with TauCeti.isCompact_setOf_lipschitzWith_apply_zero_eq_of_isCompact_closedBall its form for a compact closed ball.

References

• J. R. Munkres, Topology, 2nd ed., Prentice Hall 2000, §47 (Ascoli's theorem).

theorem ContinuousMap.isClosedEmbedding_toUniformOnFunIsCompact {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [CompactlyCoherentSpace X] [UniformSpace Y] : Topology.IsClosedEmbedding toUniformOnFunIsCompact

C(X, Y) sits inside the space of functions with the topology of uniform convergence on compacts as a closed subspace, when the topology of X is coherent with its compact sets: the coercion is a uniform embedding (ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact), and its range is the set of continuous maps, which is closed.

theorem ArzelaAscoli.isCompact_closure_range_of_equicontinuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [UniformSpace Y] {ι : Type u_3} {f : ι → C(X, Y)} (hf : Equicontinuous fun (i : ι) => ⇑(f i)) (hfpt : ∀ (x : X), ∃ (Q : Set Y), IsCompact Q ∧ ∀ (i : ι), (f i) x ∈ Q) : IsCompact (closure (Set.range f))

The Arzelà–Ascoli theorem in C(X, Y). An equicontinuous family of continuous maps whose values at each point lie in a common compact set has relatively compact range in the compact-open topology. No assumption on the topology of X is needed.

theorem EquicontinuousOn.exists_finite_approx_of_isCompact {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [UniformSpace Y] {ι : Type u_3} {g : ι → X → Y} {K : Set X} (hequi : EquicontinuousOn g K) (hK : IsCompact K) (hg : ∀ x ∈ K, TotallyBounded (Set.range fun (i : ι) => g i x)) {U : Set (Y × Y)} (hU : U ∈ uniformity Y) : ∃ (t : Set ι), t.Finite ∧ ∀ (i : ι), ∃ j ∈ t, ∀ x ∈ K, (g i x, g j x) ∈ U

An equicontinuous family with pointwise totally bounded values has a finite uniform approximation on every compact set, with approximants drawn from the family itself.

theorem ArzelaAscoli.isCompact_closure_of_equicontinuous_of_totallyBounded {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [UniformSpace Y] [CompleteSpace Y] {A : Set C(X, Y)} {D : Set X} (hD : Dense D) (hA : Equicontinuous fun (f : ↑A) => ⇑↑f) (hAD : ∀ x ∈ D, TotallyBounded ((fun (f : C(X, Y)) => f x) '' A)) : IsCompact (closure A)

The Arzelà–Ascoli theorem in C(X, Y), with a dense set of points. For a complete target Y, an equicontinuous set of continuous maps whose values are totally bounded at the points of a dense set D ⊆ X has compact closure in the compact-open topology.

theorem IsCompact.equicontinuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] [UniformSpace Y] {K : Set C(X, Y)} (hK : IsCompact K) : Equicontinuous fun (f : ↑K) => ⇑↑f

A compact set of continuous maps is equicontinuous. On a weakly locally compact space X (for instance a compact space), every compact subset of C(X, Y) is equicontinuous; this is a converse of ArzelaAscoli.isCompact_closure_range_of_equicontinuous.

theorem TauCeti.exists_tendstoUniformly_subseq_of_periodic_of_modulus {M : Type u_3} [PseudoMetricSpace M] {K : Set M} (hK : IsCompact K) {y : ℕ → ℝ → M} (hy : ∀ (n : ℕ), Continuous (y n)) (hper : ∀ (n : ℕ), Function.Periodic (y n) 1) (hyK : ∀ (n : ℕ) (t : ℝ), y n t ∈ K) {ρ : ℝ → ℝ} (hρ : Filter.Tendsto ρ (nhds 0) (nhds 0)) (hmod : ∀ (n : ℕ), ∀ t₁ ∈ Set.Icc 0 1, ∀ t₂ ∈ Set.Icc 0 1, t₁ ≤ t₂ → dist (y n t₂) (y n t₁) ≤ ρ (t₂ - t₁)) : ∃ (ψ : ℕ → ℕ), StrictMono ψ ∧ ∃ (x : ℝ → M), Function.Periodic x 1 ∧ Continuous x ∧ TendstoUniformly (fun (n : ℕ) => y (ψ n)) x Filter.atTop

Periodic Arzelà–Ascoli. A sequence of continuous 1-periodic loops in a compact set K, sharing a modulus of continuity ρ with ρ(h) → 0 as h → 0 on [0, 1], has a subsequence converging uniformly on ℝ to a continuous 1-periodic loop.

theorem TauCeti.isCompact_setOf_periodic_lipschitzWith {M : Type u_3} [MetricSpace M] {K : Set M} (hK : IsCompact K) (L : NNReal) : IsCompact {f : UniformFun ℝ M | Function.Periodic (UniformFun.toFun f) 1 ∧ (∀ (t : ℝ), UniformFun.toFun f t ∈ K) ∧ LipschitzWith L (UniformFun.toFun f)}

Periodic Arzelà–Ascoli, compact form. In the topology of uniform convergence on ℝ, the 1-periodic L-Lipschitz loops with values in a compact set K form a compact set.

theorem TauCeti.exists_subseq_tendstoLocallyUniformly_comp_add {M : Type u_3} [PseudoMetricSpace M] {K : Set M} (hK : IsCompact K) {u : ℝ × ℝ → M} {b : ℝ} {L : NNReal} (hL : LipschitzOnWith L u (Set.Ici b ×ˢ Set.univ)) (huK : Set.MapsTo u (Set.Ici b ×ˢ Set.univ) K) {σ : ℕ → ℝ} (hσ : Filter.Tendsto σ Filter.atTop Filter.atTop) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∃ (g : C(ℝ × ℝ, M)), TendstoLocallyUniformly (fun (n : ℕ) (z : ℝ × ℝ) => u (z + (σ (φ n), 0))) (⇑g) Filter.atTop

Arzelà–Ascoli for translates along an end. Let u be Lipschitz on the half-plane s ≥ b of ℝ × ℝ, with values there in a compact subset of a pseudometric space, and let σₙ → ∞. A subsequence of the translates (s, t) ↦ u(s + σₙ, t) converges locally uniformly on ℝ × ℝ to a continuous map.

theorem TauCeti.isCompact_setOf_lipschitzWith_apply_zero_eq_of_isCompact_closedBall {Y : Type u_3} [MetricSpace Y] (C : NNReal) (x : Y) (hx : IsCompact (Metric.closedBall x ↑C)) : IsCompact {f : C(↑unitInterval, Y) | LipschitzWith C ⇑f ∧ f 0 = x}

The C-Lipschitz paths on the unit interval starting at x form a compact subset of C(I, Y) when the closed ball of radius C about x is compact.

theorem TauCeti.isCompact_setOf_lipschitzWith_apply_zero_eq {Y : Type u_3} [MetricSpace Y] [ProperSpace Y] (C : NNReal) (x : Y) : IsCompact {f : C(↑unitInterval, Y) | LipschitzWith C ⇑f ∧ f 0 = x}

In a proper space, the C-Lipschitz paths on the unit interval starting at x form a compact subset of C(I, Y).