English
The inverse of the Levy-Prokhorov equivalence between probability measures is continuous.
Русский
Обратная связь эквивалентности Леви–Прокхоров между мерами непрерывна.
LaTeX
$$$\\text{Continuous }(\\mathrm{LevyProkhorov}.\\mathrm{equiv}(\\mathrm{ProbabilityMeasure}\\Omega).\\mathrm{symm})$$$
Lean4
/-- Assuming `levyProkhorovEDist μ ν < ε`, we can bound `∫ f ∂μ` in terms of
`∫ t in (0, ‖f‖], ν (thickening ε {x | f(x) ≥ t}) dt` and `‖f‖`. -/
theorem integral_le_of_levyProkhorovEDist_lt (μ ν : Measure Ω) [IsFiniteMeasure μ] [IsFiniteMeasure ν] {ε : ℝ}
(ε_pos : 0 < ε) (hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε) (f : Ω →ᵇ ℝ) (f_nn : 0 ≤ᵐ[μ] f) :
∫ ω, f ω ∂μ ≤ (∫ t in Ioc 0 ‖f‖, ν.real (thickening ε {a | t ≤ f a})) + ε * ‖f‖ :=
by
rw [BoundedContinuousFunction.integral_eq_integral_meas_le f μ f_nn]
have key : (fun (t : ℝ) ↦ μ.real {a | t ≤ f a}) ≤ (fun (t : ℝ) ↦ ν.real (thickening ε {a | t ≤ f a}) + ε) :=
by
intro t
simp only [measureReal_def]
convert
ENNReal.toReal_mono ?_ <|
left_measure_le_of_levyProkhorovEDist_lt hμν (B := {a | t ≤ f a}) (f.continuous.measurable measurableSet_Ici)
· rw [ENNReal.toReal_add (measure_ne_top ν _) ofReal_ne_top, ENNReal.toReal_ofReal ε_pos.le]
· exact ENNReal.add_ne_top.mpr ⟨measure_ne_top ν _, ofReal_ne_top⟩
have intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) :=
by
apply Measure.integrableOn_of_bounded (M := μ.real univ) measure_Ioc_lt_top.ne
· apply (Measurable.ennreal_toReal (Antitone.measurable ?_)).aestronglyMeasurable
exact fun _ _ hst ↦ measure_mono (fun _ h ↦ hst.trans h)
· apply Eventually.of_forall <| fun t ↦ ?_
simp only [Real.norm_eq_abs, abs_of_nonneg measureReal_nonneg]
exact measureReal_mono (subset_univ _)
have intble₂ : IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) (Ioc 0 ‖f‖) :=
by
apply Measure.integrableOn_of_bounded (M := ν.real univ) measure_Ioc_lt_top.ne
· apply (Measurable.ennreal_toReal (Antitone.measurable ?_)).aestronglyMeasurable
exact fun _ _ hst ↦ measure_mono <| thickening_subset_of_subset ε (fun _ h ↦ hst.trans h)
· apply Eventually.of_forall <| fun t ↦ ?_
simp only [Real.norm_eq_abs, abs_of_nonneg measureReal_nonneg]
exact ENNReal.toReal_mono (by finiteness) <| measure_mono (subset_univ _)
apply le_trans (setIntegral_mono (s := Ioc 0 ‖f‖) ?_ ?_ key)
· rw [integral_add]
· simp [(mul_comm _ ε).le]
· exact intble₂
· exact integrable_const ε
· exact intble₁
· exact intble₂.add <| integrable_const ε
