levyProkhorovDist_metricSpace_probabilityMeasure

English

If Ω is a Borel space, then the Levy-Prokhorov distance makes LevyProkhorov(ProbabilityMeasure Ω) a metric space.

Русский

Если Ω — пространство Бореля, то расстояние Леви–Прокхоров превращает пространство LevyProkhorov(ProbabilityMeasure Ω) в метрическое пространство.

LaTeX

$$$[\\text{Borel}(\\Omega)]\\; \\operatorname{levyProkhorovDist}_{\\text{pseudoMetricSpace}} (\\mu,\\nu) \\text{ defines a metric on } \\mathrm{LevyProkhorov}(\\mathrm{ProbabilityMeasure}(\\Omega)).$$$

Lean4

/-- If `Ω` is a Borel space, then the Lévy-Prokhorov distance `levyProkhorovDist` makes
`ProbabilityMeasure Ω` a metric space. The instance is recorded on the type synonym
`LevyProkhorov (ProbabilityMeasure Ω) := ProbabilityMeasure Ω`.

Note: For this metric to give the topology of convergence in distribution, one must
furthermore assume that `Ω` is separable. -/
noncomputable instance levyProkhorovDist_metricSpace_probabilityMeasure [BorelSpace Ω] :
    MetricSpace (LevyProkhorov (ProbabilityMeasure Ω)) where
  eq_of_dist_eq_zero := by
    intro μ ν h
    apply (LevyProkhorov.equiv _).injective
    apply ProbabilityMeasure.toMeasure_injective
    apply ext_of_generate_finite _ ?_ isPiSystem_isClosed ?_ (by simp)
    · rw [BorelSpace.measurable_eq (α := Ω), borel_eq_generateFrom_isClosed]
    · intro A A_closed
      apply measure_eq_measure_of_levyProkhorovEDist_eq_zero_of_isClosed
      ·
        simpa only [levyProkhorovEDist_ne_top μ.toMeasure ν.toMeasure, mem_setOf_eq, or_false, ne_eq, zero_ne_top,
          not_false_eq_true, toReal_zero] using (toReal_eq_zero_iff _).mp h
      · exact A_closed
      · exact ⟨1, Real.zero_lt_one, measure_ne_top _ _⟩
      · exact ⟨1, Real.zero_lt_one, measure_ne_top _ _⟩

Похожие утверждения