English
If f is continuous, the push-forward map ν ↦ ν.map f is continuous (in the convergence-in-distribution topology).
Русский
Если f непрерывна, отображение образующей меры в образ по f непрерывно в топологии сходимости по распределению.
LaTeX
$$$\\text{Continuous map: } \\nu \\mapsto (\\nu.map f) \\text{ is continuous in distribution}.$$$
Lean4
/-- If `f : X → Y` is continuous and `Y` is equipped with the Borel sigma algebra, then
the push-forward of probability measures `f* : ProbabilityMeasure X → ProbabilityMeasure Y`
is continuous (in the topologies of convergence in distribution). -/
theorem continuous_map {f : Ω → Ω'} (f_cont : Continuous f) :
Continuous (fun ν ↦ ProbabilityMeasure.map ν f_cont.measurable.aemeasurable) :=
by
rw [continuous_iff_continuousAt]
exact fun _ ↦ tendsto_map_of_tendsto_of_continuous _ _ continuous_id.continuousAt f_cont
