English
Equivalence with complex-valued/bounded continuous test functions: Tendsto μs F (nhds μ) iff ∀ f : Ω →ᵇ 𝕜, Tendsto ∫ f dμ_s → ∫ f dμ.
Русский
Эквивалентность слабого схождения для функций в 𝕜: Tendsto μ_s F (nhds μ) эквивалентно ∀ f: Ω →ᵇ 𝕜, Tendsto ∫ f dμ_s → ∫ f dμ.
LaTeX
$$$Tendsto μs F (nhds μ) \\iff ∀ f : Ω →ᵇ 𝕜, Tendsto (i \\mapsto ∫ f \\; d(μ_s i)) F (nhds (∫ f \\; dμ))$$$
Lean4
/-- If `f : X → Y` is continuous and `Y` is equipped with the Borel sigma algebra, then
(weak) convergence of `FiniteMeasure`s on `X` implies (weak) convergence of the push-forwards
of these measures by `f`. -/
theorem tendsto_map_of_tendsto_of_continuous {ι : Type*} {L : Filter ι} (νs : ι → FiniteMeasure Ω) (ν : FiniteMeasure Ω)
(lim : Tendsto νs L (𝓝 ν)) {f : Ω → Ω'} (f_cont : Continuous f) : Tendsto (fun i ↦ (νs i).map f) L (𝓝 (ν.map f)) :=
by
rw [FiniteMeasure.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
