English
If f is continuous between spaces with Borel structure, the pushforward map ν ↦ ν.map f is continuous in the topology of weak convergence.
Русский
Если f непрерывна между пространствами с борелевской структурой, то отображение двух мер в их образ по f непрерывно в топологии слабой сходимости.
LaTeX
$$$\\text{Continuous map: } \\nu \\mapsto (\\nu.map f) \\text{ is continuous under weak convergence.}$$$
Lean4
/-- If `f : X → Y` is continuous and `Y` is equipped with the Borel sigma algebra, then
convergence (in distribution) of `ProbabilityMeasure`s on `X` implies convergence (in
distribution) of the push-forwards of these measures by `f`. -/
theorem tendsto_map_of_tendsto_of_continuous {ι : Type*} {L : Filter ι} (νs : ι → ProbabilityMeasure Ω)
(ν : ProbabilityMeasure Ω) (lim : Tendsto νs L (𝓝 ν)) {f : Ω → Ω'} (f_cont : Continuous f) :
Tendsto (fun i ↦ (νs i).map f_cont.measurable.aemeasurable) L (𝓝 (ν.map f_cont.measurable.aemeasurable)) :=
by
rw [ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto] at lim ⊢
intro g
convert lim (g.compContinuous ⟨f, f_cont⟩) <;>
· simp only [map, compContinuous_apply, ContinuousMap.coe_mk]
refine lintegral_map ?_ f_cont.measurable
exact (ENNReal.continuous_coe.comp g.continuous).measurable
