English
There is a continuous equivalence between Levy-Prokhorov space of probability measures and the space of probability measures, establishing a canonical bridge between the metric and weak topologies.
Русский
Существует непрерывное эквивалентное отображение между пространством Леви–Прокхоровых мер и пространством вероятностных мер, соединяющее метрическое и слабое топологические структуры.
LaTeX
$$$\\text{Continuous }(\\mathrm{LevyProkhorov.equiv}(\\alpha := \\mathrm{ProbabilityMeasure }\\Omega)) \\quad \\Rightarrow \\quad \\text{topological relation with probability measures.}$$$
Lean4
/-- A version of the layer cake formula for bounded continuous functions which have finite integral:
∫ f dμ = ∫ t in (0, ‖f‖], μ {x | f(x) ≥ t} dt. -/
theorem integral_eq_integral_meas_le_of_hasFiniteIntegral {α : Type*} [MeasurableSpace α] [TopologicalSpace α]
[OpensMeasurableSpace α] (f : α →ᵇ ℝ) (μ : Measure α) (f_nn : 0 ≤ᵐ[μ] f) (hf : HasFiniteIntegral f μ) :
∫ ω, f ω ∂μ = ∫ t in Ioc 0 ‖f‖, μ.real {a : α | t ≤ f a} :=
by
rw [Integrable.integral_eq_integral_Ioc_meas_le (M := ‖f‖) ?_ f_nn ?_]
· exact ⟨f.continuous.measurable.aestronglyMeasurable, hf⟩
· exact Eventually.of_forall (fun x ↦ BoundedContinuousFunction.apply_le_norm f x)
