Laws on spaces of continuous maps

A law on the path space C(T, E) whose time marginals at the times of a countable dense set are concentrated on a closed set F is concentrated on the paths with values in F at all times. When F is the range of a closed embedding ι : X → E, the law is therefore the image of a law on C(T, X) under postcomposition with ι.

Main results

• TauCeti.ae_forall_apply_mem_of_dense: a law on continuous paths whose time marginals at the times of a countable dense set are concentrated on a closed set is concentrated on the paths with values in that set.
• TauCeti.isProbabilityMeasure_comap_postcomp: such a law can be pulled back along a closed embedding of the path codomain.

theorem TauCeti.ae_forall_apply_mem_of_dense {T : Type u_1} {E : Type u_2} [TopologicalSpace T] [TopologicalSpace E] [MeasurableSpace C(T, E)] {η : MeasureTheory.Measure C(T, E)} {D : Set T} (hDc : D.Countable) (hDd : Dense D) {F : Set E} (hF : IsClosed F) (h : ∀ t ∈ D, ∀ᵐ (γ : C(T, E)) ∂η, γ t ∈ F) : ∀ᵐ (γ : C(T, E)) ∂η, ∀ (t : T), γ t ∈ F

A law on paths C(T, E) whose time marginals at the times of a countable dense set D are concentrated on a closed set F is concentrated on the paths with values in F at all times.

theorem TauCeti.isProbabilityMeasure_comap_postcomp {T : Type u_1} {X : Type u_2} {E : Type u_3} [TopologicalSpace T] [TopologicalSpace X] [TopologicalSpace E] [T2Space E] [PolishSpace C(T, X)] (ι : X → E) (hι : Topology.IsClosedEmbedding ι) (η : MeasureTheory.Measure C(T, E)) (hη : MeasureTheory.IsProbabilityMeasure η) {D : Set T} (hDc : D.Countable) (hDd : Dense D) (hD : ∀ t ∈ D, ∀ᵐ (γ : C(T, E)) ∂η, γ t ∈ Set.range ι) : MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.comap { toFun := ι, continuous_toFun := ⋯ }.comp η) ∧ MeasureTheory.Measure.map { toFun := ι, continuous_toFun := ⋯ }.comp (MeasureTheory.Measure.comap { toFun := ι, continuous_toFun := ⋯ }.comp η) = η

Pulling a probability law on C(T, E) back along postcomposition by a closed embedding ι : X → E gives a probability law whose pushforward is the original law, provided the original law is concentrated on paths valued in the range of ι at the times of a countable dense set.