English
A collection of simple equivalence lemmas shows that the symmetric and union/intersection structure of sets behaves as expected under Levy–Prokhorov equivalence.
Русский
Леммы простых равносвязей показывают корректность поведения симметрии и операций над множествами при эквивалентности Леви–Прокхоровой.
LaTeX
$$$\\text{simp_lemma} : \\exists \\text{ structure on sets compatible with } \\mathrm{LevyProkhorov}. $$$
Lean4
theorem toMeasure_add_pos_gt_mem_nhds (P : ProbabilityMeasure Ω) {G : Set Ω} (G_open : IsOpen G) {ε : ℝ≥0∞}
(ε_pos : 0 < ε) : {Q | P.toMeasure G < Q.toMeasure G + ε} ∈ 𝓝 P :=
by
by_cases easy : P.toMeasure G < ε
· exact Eventually.of_forall (fun _ ↦ lt_of_lt_of_le easy le_add_self)
by_cases ε_top : ε = ∞
· simp [ε_top, measure_lt_top]
simp only [not_lt] at easy
have aux : P.toMeasure G - ε < liminf (fun Q ↦ Q.toMeasure G) (𝓝 P) :=
by
apply
lt_of_lt_of_le (ENNReal.sub_lt_self (by finiteness) _ _) <|
ProbabilityMeasure.le_liminf_measure_open_of_tendsto tendsto_id G_open
· exact (lt_of_lt_of_le ε_pos easy).ne.symm
· exact ε_pos.ne.symm
filter_upwards [gt_mem_sets_of_limsInf_gt (α := ℝ≥0∞) isBounded_ge_of_bot
(show P.toMeasure G - ε < limsInf ((𝓝 P).map (fun Q ↦ Q.toMeasure G)) from aux)] with
Q hQ
simp only [preimage_setOf_eq, mem_setOf_eq] at hQ
convert ENNReal.add_lt_add_right ε_top hQ
exact (tsub_add_cancel_of_le easy).symm
