Continuous pushforwards of probability measures

A continuous measurable map induces a continuous pushforward for the weak topologies on probability measures. Both spaces need measurable opens, but their sigma algebras may be finer than the Borel sigma algebras. This applies in particular to measurable coordinate projections when the product topology has measurable opens.

MeasureTheory.ProbabilityMeasure.continuous_map_of_measurable extends Mathlib's MeasureTheory.ProbabilityMeasure.continuous_map by making the map's measurability explicit instead of requiring the target's measurable space to be Borel. Its proof uses the same bounded-continuous-test-function characterization of weak convergence.

MeasureTheory.ProbabilityMeasure.continuous_map_of_forall_continuous: the laws of a family of random variables that depends continuously on a parameter, for every outcome, depend continuously on that parameter. For example, the time marginals of a law on a space of continuous paths form a continuous curve of probability measures.

MeasureTheory.ProbabilityMeasure.continuous_map_of_continuous_uncurry allows the input law to vary together with the parameter of a jointly continuous map. It combines Mathlib's ProbabilityMeasure.continuous_prod and continuous_diracProba by representing the parameter as a Dirac factor.

theorem MeasureTheory.ProbabilityMeasure.continuous_map_of_measurable {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] [TopologicalSpace X] [OpensMeasurableSpace X] [TopologicalSpace Y] [OpensMeasurableSpace Y] {f : X → Y} (hf : Continuous f) (hm : Measurable f) : Continuous fun (μ : ProbabilityMeasure X) => μ.map f

A continuous measurable map induces a continuous pushforward of probability measures for the weak topologies, even when the target's measurable space is finer than its Borel space.

theorem MeasureTheory.ProbabilityMeasure.continuous_map_of_continuous_uncurry {T : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace T] [SecondCountableTopology T] [TopologicalSpace.PseudoMetrizableSpace T] [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] [SecondCountableTopology X] [TopologicalSpace.PseudoMetrizableSpace X] [TopologicalSpace Y] [MeasurableSpace Y] [BorelSpace Y] {f : T → X → Y} (hf : Continuous (Function.uncurry f)) : Continuous fun (p : T × ProbabilityMeasure X) => p.2.map (f p.1)

Pushforward by a jointly continuous map depends weakly continuously on both its parameter and its input probability law.

theorem MeasureTheory.ProbabilityMeasure.continuous_map_of_forall_continuous {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [TopologicalSpace T] [FirstCountableTopology T] [MeasurableSpace Ω] [TopologicalSpace E] [MeasurableSpace E] [OpensMeasurableSpace E] (P : ProbabilityMeasure Ω) {f : T → Ω → E} (hf : ∀ (t : T), AEMeasurable (f t) ↑P) (hcont : ∀ (ω : Ω), Continuous fun (t : T) => f t ω) : Continuous fun (t : T) => P.map (f t)

If f t ω depends continuously on t for every ω, then the laws P.map (f t) depend continuously on t for the weak topology. For instance, the time marginals of a law on a space of continuous paths form a continuous curve.