Tightness of laws on a space of continuous curves

Let α be a compact pseudometric space, for instance a compact time interval [0, T], and let X be a complete metric space. This file characterizes the tight sets of measures on the space C(α, X) of continuous curves, with its compact-open (equivalently, uniform) topology. A set S of measures on C(α, X) is tight exactly when

• its time marginals are tight: for every t in a dense set D ⊆ α, the laws of the evaluation γ ↦ γ t under the members of S form a tight set of measures on X; and
• it satisfies a uniform modulus of continuity in probability: for all η, ε > 0 there is δ > 0 such that, for every P ∈ S, the curves γ having two times s, t with dist s t < δ and η ≤ dist (γ s) (γ t) have P-measure at most ε.

The sufficiency result also holds for a Lindelöf pseudometric domain α, for instance ℝ, and a complete pseudometric target X, with the compact-open topology on C(α, X). Compactness of α is needed for the converse.

This is the tightness criterion used to extract limits of laws of random curves, for instance in the superposition principle for absolutely continuous curves of probability measures. The sufficiency of the two conditions is proved by intersecting countably many events of large measure, each controlling either the oscillation of the curves at one scale or their position at one time of a countable dense subset of D. The resulting set of curves is equicontinuous with values in a compact set at each of these times, so it has compact closure by the Arzelà–Ascoli theorem ArzelaAscoli.isCompact_closure_of_equicontinuous_of_totallyBounded. Completeness of X is what turns total boundedness of the values at the remaining times into compactness; the modulus condition is stated for arbitrary sets of curves, with no measurability requirement, because measures are outer measures.

Without a hypothesis on the time marginals the modulus condition is not enough when X is not proper: the Dirac masses at the curves t • eₙ of TauCeti.exists_lipschitzWith_one_not_isCompact_closure_range satisfy it, since all these curves are 1-Lipschitz, but they do not form a tight set.

Main results

• TauCeti.isTightMeasureSet_of_map_eval_of_continuity_modulus: tight time marginals on a dense set of times and a uniform modulus of continuity in probability give tightness.
• MeasureTheory.IsTightMeasureSet.exists_measure_continuity_modulus_le: conversely, a tight set of measures on C(α, X) satisfies the uniform modulus of continuity in probability.
• TauCeti.isTightMeasureSet_iff_map_eval_and_continuity_modulus: the characterization.

References

• P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley 1999, Theorem 7.3, the case of real-valued curves on [0, 1], where tightness of the marginal at the single time 0 suffices.

theorem MeasureTheory.IsTightMeasureSet.exists_measure_continuity_modulus_le {α : Type u_1} {X : Type u_2} [PseudoMetricSpace α] [PseudoMetricSpace X] [MeasurableSpace C(α, X)] {S : Set (Measure C(α, X))} [CompactSpace α] (hS : IsTightMeasureSet S) (η : ℝ) : η > 0 → ∀ ε > 0, ∃ δ > 0, ∀ P ∈ S, P {γ : C(α, X) | ∃ (s : α) (t : α), dist s t < δ ∧ η ≤ dist (γ s) (γ t)} ≤ ε

A tight set of laws of curves has a uniform modulus of continuity in probability. If S is a tight set of measures on C(α, X), then for all η, ε > 0 there is δ > 0 such that, for every P ∈ S, the curves with two times closer than δ at which their values are at least η apart have P-measure at most ε.

theorem TauCeti.isTightMeasureSet_of_map_eval_of_continuity_modulus {α : Type u_1} {X : Type u_2} [PseudoMetricSpace α] [PseudoMetricSpace X] [MeasurableSpace C(α, X)] {S : Set (MeasureTheory.Measure C(α, X))} [MeasurableSpace X] [BorelSpace X] [OpensMeasurableSpace C(α, X)] {D : Set α} [LindelofSpace α] [CompleteSpace X] (hD : Dense D) (h_eval : ∀ t ∈ D, MeasureTheory.IsTightMeasureSet ((fun (P : MeasureTheory.Measure C(α, X)) => MeasureTheory.Measure.map (fun (γ : C(α, X)) => γ t) P) '' S)) (h_mod : ∀ η > 0, ∀ ε > 0, ∃ δ > 0, ∀ P ∈ S, P {γ : C(α, X) | ∃ (s : α) (t : α), dist s t < δ ∧ η ≤ dist (γ s) (γ t)} ≤ ε) : MeasureTheory.IsTightMeasureSet S

Tightness criterion for laws of curves. Let α be a Lindelöf pseudometric space, X a complete pseudometric space, and D ⊆ α dense. A set S of measures on C(α, X) is tight if its time marginals at the times of D are tight and it satisfies a uniform modulus of continuity in probability: for all η, ε > 0 there is δ > 0 such that, for every P ∈ S, the curves with two times closer than δ at which their values are at least η apart have P-measure at most ε.

theorem TauCeti.isTightMeasureSet_iff_map_eval_and_continuity_modulus {α : Type u_1} {X : Type u_2} [PseudoMetricSpace α] [PseudoMetricSpace X] [MeasurableSpace C(α, X)] {S : Set (MeasureTheory.Measure C(α, X))} [MeasurableSpace X] [BorelSpace X] [OpensMeasurableSpace C(α, X)] {D : Set α} [CompactSpace α] [CompleteSpace X] [T2Space X] (hD : Dense D) : MeasureTheory.IsTightMeasureSet S ↔ (∀ t ∈ D, MeasureTheory.IsTightMeasureSet ((fun (P : MeasureTheory.Measure C(α, X)) => MeasureTheory.Measure.map (fun (γ : C(α, X)) => γ t) P) '' S)) ∧ ∀ η > 0, ∀ ε > 0, ∃ δ > 0, ∀ P ∈ S, P {γ : C(α, X) | ∃ (s : α) (t : α), dist s t < δ ∧ η ≤ dist (γ s) (γ t)} ≤ ε

Characterization of tight laws of curves. Let X be a complete metric space and D ⊆ α dense. A set S of measures on C(α, X) is tight if and only if its time marginals at the times of D are tight and it satisfies a uniform modulus of continuity in probability.