A refined Arzelà–Ascoli theorem for maps with an asymptotic modulus

Let v k : T → X be a sequence of maps from a separable topological space T to an extended metric space X, or more generally a weak extended metric space. The maps need not be continuous: they are only asked to be asymptotically equicontinuous, in the sense that

limsup_k d(v k s, v k t) ≤ ω s t

for a function ω with ω t s → 0 as s → t. The values are compared through an auxiliary convergence y_n ⇀ y on X, given by filters l y, which may be weaker than that of the metric but for which the distance is jointly lower semicontinuous. If the values at each time lie in a set that is relatively sequentially compact for ⇀, then a subsequence of the maps converges pointwise for ⇀ to a map u with d(u s, u t) ≤ ω s t (TauCeti.tendsto_subseq_of_limsup_edist_le).

This is the compactness theorem behind the convergence of the minimizing movement scheme. The piecewise constant interpolants of the scheme jump at every time step, so they are not equicontinuous, but the jumps vanish as the time step tends to zero. In the Wasserstein space the auxiliary convergence is narrow convergence. Relative narrow compactness of bounded energy sublevels is then a hypothesis on the energy and the underlying space; it holds, for instance, over a proper underlying space, where bounded sets are tight, although they need not be relatively compact for the metric.

The proof extracts, by a diagonal argument, a subsequence converging at the points of a countable dense set. At any other time t, two limits of further subsequences are both within ω t s of the limit at every point s of the dense set, so they coincide, and the whole subsequence converges.

Main results

• TauCeti.tendsto_subseq_of_limsup_edist_le: the refined Arzelà–Ascoli theorem.

References

• L. Ambrosio, N. Gigli, G. Savaré, Gradient Flows in Metric Spaces and in the Space of Probability Measures, 2nd ed., Birkhäuser 2008, Proposition 3.3.1.

theorem TauCeti.tendsto_subseq_of_limsup_edist_le {T : Type u_1} {X : Type u_2} [TopologicalSpace T] [TopologicalSpace X] [WeakEMetricSpace X] {l : X → Filter X} [TopologicalSpace.SeparableSpace T] (hd : ∀ ⦃v w : ℕ → X⦄ ⦃y z : X⦄, Filter.Tendsto v Filter.atTop (l y) → Filter.Tendsto w Filter.atTop (l z) → edist y z ≤ Filter.liminf (fun (n : ℕ) => edist (v n) (w n)) Filter.atTop) {v : ℕ → T → X} {K : T → Set X} (hvK : ∀ (k : ℕ) (t : T), v k t ∈ K t) (hK : ∀ (t : T) ⦃w : ℕ → X⦄, (∀ (n : ℕ), w n ∈ K t) → ∃ (y : X) (ψ : ℕ → ℕ), StrictMono ψ ∧ Filter.Tendsto (w ∘ ψ) Filter.atTop (l y)) {ω : T → T → ENNReal} (hvω : ∀ (s t : T), Filter.limsup (fun (k : ℕ) => edist (v k s) (v k t)) Filter.atTop ≤ ω s t) (hω : ∀ (t : T), Filter.Tendsto (ω t) (nhds t) (nhds 0)) : ∃ (ψ : ℕ → ℕ), StrictMono ψ ∧ ∃ (u : T → X), (∀ (t : T), Filter.Tendsto (fun (n : ℕ) => v (ψ n) t) Filter.atTop (l (u t))) ∧ ∀ (s t : T), edist (u s) (u t) ≤ ω s t

A refined Arzelà–Ascoli theorem (Ambrosio–Gigli–Savaré, Proposition 3.3.1). Let l y be the filter of an auxiliary convergence y_n ⇀ y on a weak extended metric space X, for which the distance is jointly sequentially lower semicontinuous. The topology of X need not be induced by its extended distance; the auxiliary convergence is specified only by l. Let v k : T → X be maps on a separable space T such that

• at each time t, the values v k t lie in a set K t in which every sequence has a ⇀-convergent subsequence;
• limsup_k d(v k s, v k t) ≤ ω s t, where ω t s → 0 as s → t.

Then a subsequence v (ψ n) converges pointwise for ⇀ to a map u : T → X with d(u s, u t) ≤ ω s t. The maps v k need not be continuous.