English
The Lévy-Prokhorov topology on ProbabilityMeasure Ω coincides with the topology of convergence in distribution (for separable Ω).
Русский
Топология Леви–Прокхоровой мер на ProbabilityMeasure Ω совпадает с топологией сходимости по распределению (для разделимого пространства).
LaTeX
$$$\\mathrm{ProbabilityMeasure}(Ω)$ имеет ту же топологию, что и топология схождения по распределению, через эквивалентность Леви–Прокхорову.$$
Lean4
/-- The identity map `LevyProkhorov (ProbabilityMeasure Ω) → ProbabilityMeasure Ω` is continuous. -/
theorem continuous_equiv_probabilityMeasure : Continuous (LevyProkhorov.equiv (α := ProbabilityMeasure Ω)) :=
by
refine SeqContinuous.continuous ?_
intro μs ν hμs
set P := LevyProkhorov.equiv _ ν
set Ps := fun n ↦
LevyProkhorov.equiv _
(μs n) -- more palatable notation
rw [ProbabilityMeasure.tendsto_iff_forall_integral_tendsto]
refine fun f ↦ tendsto_integral_of_forall_limsup_integral_le_integral ?_ f
intro f f_nn
by_cases f_zero : ‖f‖ = 0
· simp only [norm_eq_zero] at f_zero
simp [f_zero, limsup_const]
have norm_f_pos : 0 < ‖f‖ := lt_of_le_of_ne (norm_nonneg _) (fun a => f_zero a.symm)
apply _root_.le_of_forall_pos_le_add
intro δ δ_pos
apply limsup_le_of_le ?_
· obtain ⟨εs, ⟨_, ⟨εs_pos, εs_lim⟩⟩⟩ := exists_seq_strictAnti_tendsto (0 : ℝ)
have ε_of_room := Tendsto.add (tendsto_iff_dist_tendsto_zero.mp hμs) εs_lim
have ε_of_room' : Tendsto (fun n ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0) :=
by
rw [tendsto_nhdsWithin_iff]
refine ⟨by simpa using ε_of_room, Eventually.of_forall fun n ↦ ?_⟩
· rw [mem_Ioi]
linarith [εs_pos n, dist_nonneg (x := μs n) (y := ν)]
rw [add_zero] at ε_of_room
have key := (tendsto_integral_meas_thickening_le f (A := Ioc 0 ‖f‖) (by simp) P).comp ε_of_room'
have aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z := fun z ↦ Iio_mem_nhds (by linarith)
filter_upwards [key (aux _), ε_of_room <| Iio_mem_nhds <| half_pos <| mul_pos (inv_pos.mpr norm_f_pos) δ_pos] with n
hn hn'
simp only [mem_preimage, mem_Iio] at *
specialize εs_pos n
have bound :=
BoundedContinuousFunction.integral_le_of_levyProkhorovEDist_lt (Ps n) P (ε := dist (μs n) ν + εs n) ?_ ?_ f ?_
· refine bound.trans ?_
apply (add_le_add_right hn.le _).trans
rw [BoundedContinuousFunction.integral_eq_integral_meas_le]
· rw [add_assoc, mul_comm]
gcongr
calc
δ / 2 + ‖f‖ * (dist (μs n) ν + εs n)
_ ≤ δ / 2 + ‖f‖ * (‖f‖⁻¹ * δ / 2) := by gcongr
_ = δ := by field_simp; ring
· exact Eventually.of_forall f_nn
· positivity
· rw [ENNReal.ofReal_add (by positivity) (by positivity), ← add_zero (levyProkhorovEDist _ _)]
apply ENNReal.add_lt_add_of_le_of_lt (levyProkhorovEDist_ne_top _ _) (le_of_eq ?_) (ofReal_pos.mpr εs_pos)
rw [LevyProkhorov.dist_def, levyProkhorovDist, ofReal_toReal (levyProkhorovEDist_ne_top _ _)]
rfl
· exact Eventually.of_forall f_nn
· simp only [IsCoboundedUnder, IsCobounded, eventually_map, eventually_atTop, forall_exists_index]
refine ⟨0, fun a i hia ↦ le_trans (integral_nonneg f_nn) (hia i le_rfl)⟩
