English
If two measures μ and ν on Ω have Lévy–Prokhorov distance 0, and S is a measurable set with a finite thickening under some positive δ, then μ(S) is bounded by ν(closure S).
Русский
Если две меры μ, ν на Ω имеют расстояние Леви–Прокхорово равное нулю, и S — измеримое множество с конечным объёмом под любой положительный коэффициент дельты после «размытия» (thickening), то μ(S) ограничено ν(closure S).
LaTeX
$$$\\forall \\mu\\nu : \\mathrm{Measure}(\\Omega),\\quad \\operatorname{levyProkhorovEDist}(\\mu,\\nu)=0 \\Rightarrow \\forall s\\, (\\text{MeasurableSet } s) \\(\\exists \\delta>0,\\ \\nu(\\mathrm{thickening}(\\delta\,s))<\\infty) \\Rightarrow \\mu(s) \\leq \\nu(\\overline{s}).$$$
Lean4
theorem measure_le_measure_closure_of_levyProkhorovEDist_eq_zero {μ ν : Measure Ω} (hLP : levyProkhorovEDist μ ν = 0)
{s : Set Ω} (s_mble : MeasurableSet s) (h_finite : ∃ δ > 0, ν (thickening δ s) ≠ ∞) : μ s ≤ ν (closure s) :=
by
have key : Tendsto (fun ε ↦ ν (thickening ε.toReal s)) (𝓝[>] (0 : ℝ≥0∞)) (𝓝 (ν (closure s))) :=
by
have aux : Tendsto ENNReal.toReal (𝓝[>] 0) (𝓝[>] 0) :=
by
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within (s := Ioi 0) ENNReal.toReal
· exact tendsto_nhdsWithin_of_tendsto_nhds (continuousAt_toReal zero_ne_top).tendsto
· filter_upwards [Ioo_mem_nhdsGT zero_lt_one] with x hx
exact toReal_pos hx.1.ne' <| ne_top_of_lt hx.2
exact (tendsto_measure_thickening h_finite).comp aux
have obs := Tendsto.add key (tendsto_nhdsWithin_of_tendsto_nhds tendsto_id)
simp only [id_eq, add_zero] at obs
apply ge_of_tendsto (b := μ s) obs
filter_upwards [self_mem_nhdsWithin] with ε ε_pos
exact left_measure_le_of_levyProkhorovEDist_lt (B_mble := s_mble) (hLP ▸ ε_pos)
