English
If levyProkhorovEDist(μ, ν) = 0 and s is closed, with nontrivial thickening finiteness conditions for μ and ν, then μ(s) = ν(s).
Русский
Если расстояние Леви–Прокхоров от μ до ν равно нулю и множество s замкнуто, при некоторых технических условиях на толщину для μ и ν, то μ(s) = ν(s).
LaTeX
$$$\\forall \\mu,\\nu : \\mathrm{Measure}(\\Omega),\\quad \\operatorname{levyProkhorovEDist}(\\mu,\\nu)=0 \\land IsClosed(s) \\land (\\exists \\delta>0, \\mu(\\mathrm{thickening}(\\delta\,s))\\neq \\infty) \\land (\\exists \\delta'>0, \\nu(\\mathrm{thickening}(\\delta'\,s))\\neq \\infty) \\Rightarrow \\mu(s)=\\nu(s).$$$
Lean4
/-- Two measures at vanishing Lévy-Prokhorov distance from each other assign the same values to all
closed sets. -/
theorem measure_eq_measure_of_levyProkhorovEDist_eq_zero_of_isClosed {μ ν : Measure Ω}
(hLP : levyProkhorovEDist μ ν = 0) {s : Set Ω} (s_closed : IsClosed s) (hμs : ∃ δ > 0, μ (thickening δ s) ≠ ∞)
(hνs : ∃ δ > 0, ν (thickening δ s) ≠ ∞) : μ s = ν s :=
by
apply le_antisymm
·
exact
measure_le_measure_closure_of_levyProkhorovEDist_eq_zero hLP s_closed.measurableSet hνs |>.trans <|
le_of_eq (congr_arg _ s_closed.closure_eq)
·
exact
measure_le_measure_closure_of_levyProkhorovEDist_eq_zero (levyProkhorovEDist_comm μ ν ▸ hLP)
s_closed.measurableSet hμs |>.trans <|
le_of_eq (congr_arg _ s_closed.closure_eq)
