The Lévy-Prokhorov distance on spaces of finite measures and probability measures

Main definitions

• MeasureTheory.levyProkhorovEDist: The Lévy-Prokhorov edistance between two measures.
• MeasureTheory.levyProkhorovDist: The Lévy-Prokhorov distance between two finite measures.

Main results

• LevyProkhorov.instPseudoMetricSpaceFiniteMeasure: The Lévy-Prokhorov distance is a pseudometric on the space of finite measures.
• LevyProkhorov.instPseudoMetricSpaceProbabilityMeasure: The Lévy-Prokhorov distance is a pseudometric on the space of probability measures.
• LevyProkhorov.le_convergenceInDistribution: The topology of the Lévy-Prokhorov metric on probability measures is always at least as fine as the topology of convergence in distribution.
• LevyProkhorov.eq_convergenceInDistribution: The topology of the Lévy-Prokhorov metric on probability measures on a separable space coincides with the topology of convergence in distribution, and in particular convergence in distribution is then pseudometrizable.

Tags

finite measure, probability measure, weak convergence, convergence in distribution, metrizability

Lévy-Prokhorov metric

noncomputable def MeasureTheory.levyProkhorovEDist {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] (μ ν : Measure Ω) : ENNReal

The Lévy-Prokhorov edistance between measures: d(μ,ν) = inf {r ≥ 0 | ∀ B, μ B ≤ ν Bᵣ + r ∧ ν B ≤ μ Bᵣ + r}.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.meas_le_of_le_of_forall_le_meas_thickening_add {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] {ε₁ ε₂ : ENNReal} (μ ν : Measure Ω) (h_le : ε₁ ≤ ε₂) {B : Set Ω} (hε₁ : μ B ≤ ν (Metric.thickening ε₁.toReal B) + ε₁) : μ B ≤ ν (Metric.thickening ε₂.toReal B) + ε₂

theorem MeasureTheory.left_measure_le_of_levyProkhorovEDist_lt {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] {μ ν : Measure Ω} {c : ENNReal} (h : levyProkhorovEDist μ ν < c) {B : Set Ω} (B_mble : MeasurableSet B) : μ B ≤ ν (Metric.thickening c.toReal B) + c

theorem MeasureTheory.right_measure_le_of_levyProkhorovEDist_lt {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] {μ ν : Measure Ω} {c : ENNReal} (h : levyProkhorovEDist μ ν < c) {B : Set Ω} (B_mble : MeasurableSet B) : ν B ≤ μ (Metric.thickening c.toReal B) + c

theorem MeasureTheory.levyProkhorovEDist_le_of_forall_add_pos_le {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] (μ ν : Measure Ω) (δ : ENNReal) (h : ∀ (ε : ENNReal) (B : Set Ω), 0 < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (Metric.thickening (δ + ε).toReal B) + δ + ε ∧ ν B ≤ μ (Metric.thickening (δ + ε).toReal B) + δ + ε) : levyProkhorovEDist μ ν ≤ δ

A general sufficient condition for bounding levyProkhorovEDist from above.

theorem MeasureTheory.levyProkhorovEDist_le_of_forall {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] (μ ν : Measure Ω) (δ : ENNReal) (h : ∀ (ε : ENNReal) (B : Set Ω), δ < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (Metric.thickening ε.toReal B) + ε ∧ ν B ≤ μ (Metric.thickening ε.toReal B) + ε) : levyProkhorovEDist μ ν ≤ δ

A simple general sufficient condition for bounding levyProkhorovEDist from above.

theorem MeasureTheory.levyProkhorovEDist_le_max_measure_univ {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] (μ ν : Measure Ω) : levyProkhorovEDist μ ν ≤ max (μ Set.univ) (ν Set.univ)

@[simp]

theorem MeasureTheory.levyProkhorovEDist_lt_top {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] (μ ν : Measure Ω) [IsFiniteMeasure μ] [IsFiniteMeasure ν] : levyProkhorovEDist μ ν < ⊤

@[simp]

theorem MeasureTheory.levyProkhorovEDist_ne_top {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] (μ ν : Measure Ω) [IsFiniteMeasure μ] [IsFiniteMeasure ν] : levyProkhorovEDist μ ν ≠ ⊤

@[simp]

theorem MeasureTheory.levyProkhorovEDist_self {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] (μ : Measure Ω) : levyProkhorovEDist μ μ = 0

theorem MeasureTheory.levyProkhorovEDist_comm {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] (μ ν : Measure Ω) : levyProkhorovEDist μ ν = levyProkhorovEDist ν μ

theorem MeasureTheory.levyProkhorovEDist_triangle {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] (μ ν κ : Measure Ω) : levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ

noncomputable def MeasureTheory.levyProkhorovDist {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] (μ ν : Measure Ω) : ℝ

The Lévy-Prokhorov distance between finite measures: d(μ,ν) = inf {r ≥ 0 | ∀ B, μ B ≤ ν Bᵣ + r ∧ ν B ≤ μ Bᵣ + r}.

Equations

• MeasureTheory.levyProkhorovDist μ ν = (MeasureTheory.levyProkhorovEDist μ ν).toReal

theorem MeasureTheory.levyProkhorovDist_self {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] (μ : Measure Ω) : levyProkhorovDist μ μ = 0

theorem MeasureTheory.levyProkhorovDist_comm {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] (μ ν : Measure Ω) : levyProkhorovDist μ ν = levyProkhorovDist ν μ

theorem MeasureTheory.levyProkhorovDist_triangle {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] (μ ν κ : Measure Ω) [IsFiniteMeasure μ] [IsFiniteMeasure ν] [IsFiniteMeasure κ] : levyProkhorovDist μ κ ≤ levyProkhorovDist μ ν + levyProkhorovDist ν κ

theorem MeasureTheory.measure_le_measure_closure_of_levyProkhorovEDist_eq_zero {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] {μ ν : Measure Ω} (hLP : levyProkhorovEDist μ ν = 0) {s : Set Ω} (s_mble : MeasurableSet s) (h_finite : ∃ δ > 0, ν (Metric.thickening δ s) ≠ ⊤) : μ s ≤ ν (closure s)

theorem MeasureTheory.measure_eq_measure_of_levyProkhorovEDist_eq_zero_of_isClosed {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] {μ ν : Measure Ω} (hLP : levyProkhorovEDist μ ν = 0) {s : Set Ω} (s_closed : IsClosed s) (hμs : ∃ δ > 0, μ (Metric.thickening δ s) ≠ ⊤) (hνs : ∃ δ > 0, ν (Metric.thickening δ s) ≠ ⊤) : μ s = ν s

Two measures at vanishing Lévy-Prokhorov distance from each other assign the same values to all closed sets.

theorem MeasureTheory.levyProkhorovEDist_le_of_forall_le {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] (μ ν : Measure Ω) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (δ : ENNReal) (h : ∀ (ε : ENNReal) (B : Set Ω), δ < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (Metric.thickening ε.toReal B) + ε) : levyProkhorovEDist μ ν ≤ δ

A simple sufficient condition for bounding levyProkhorovEDist between probability measures from above. The condition involves only one of two natural bounds, the other bound is for free.

theorem MeasureTheory.levyProkhorovDist_le_of_forall_le {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] (μ ν : Measure Ω) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] {δ : ℝ} (δ_nn : 0 ≤ δ) (h : ∀ (ε : ℝ) (B : Set Ω), δ < ε → MeasurableSet B → μ B ≤ ν (Metric.thickening ε B) + ENNReal.ofReal ε) : levyProkhorovDist μ ν ≤ δ

A simple sufficient condition for bounding levyProkhorovDist between probability measures from above. The condition involves only one of two natural bounds, the other bound is for free.

Equipping measures with the Lévy-Prokhorov metric

structure MeasureTheory.LevyProkhorov (α : Type u_2) : Type u_2

A type synonym, to be used for Measure α, FiniteMeasure α, or ProbabilityMeasure α, when they are to be equipped with the Lévy-Prokhorov distance.

• ofMeasure :: (
• toMeasure : α

  Turn an element of the space of measure equipped with the Lévy-Prokhorov metric into the corresponding measure.

• )

def MeasureTheory.LevyProkhorov.delabOfMeasure : Lean.PrettyPrinter.Delaborator.Delab

This prevents ofMeasure x being printed as { toMeasure := x } by delabStructureInstance.

Equations

• MeasureTheory.LevyProkhorov.delabOfMeasure = Lean.PrettyPrinter.Delaborator.delabApp

theorem MeasureTheory.LevyProkhorov.toMeasure_injective {α : Type u_2} : Function.Injective toMeasure

def MeasureTheory.LevyProkhorov.toMeasureEquiv {α : Type u_2} : LevyProkhorov α ≃ α

LevyProkhorov.toMeasure as an equiv.

Equations

• MeasureTheory.LevyProkhorov.toMeasureEquiv = { toFun := MeasureTheory.LevyProkhorov.toMeasure, invFun := MeasureTheory.LevyProkhorov.ofMeasure, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem MeasureTheory.LevyProkhorov.toMeasureEquiv_symm_apply_toMeasure {α : Type u_2} (toMeasure : α) : (toMeasureEquiv.symm toMeasure).toMeasure = toMeasure

@[simp]

theorem MeasureTheory.LevyProkhorov.toMeasureEquiv_apply {α : Type u_2} (self : LevyProkhorov α) : toMeasureEquiv self = self.toMeasure

@[deprecated MeasureTheory.LevyProkhorov.toMeasureEquiv (since := "2025-10-28")]

def MeasureTheory.LevyProkhorov.equiv {α : Type u_2} : LevyProkhorov α ≃ α

Alias of MeasureTheory.LevyProkhorov.toMeasureEquiv.

---

LevyProkhorov.toMeasure as an equiv.

Equations

• @MeasureTheory.LevyProkhorov.equiv = @MeasureTheory.LevyProkhorov.toMeasureEquiv

noncomputable instance MeasureTheory.LevyProkhorov.instPseudoEMetricSpaceMeasure {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] : PseudoEMetricSpace (LevyProkhorov (Measure Ω))

The Lévy-Prokhorov distance levyProkhorovEDist makes Measure Ω a pseudoemetric space. The instance is recorded on the type synonym LevyProkhorov (Measure Ω) := Measure Ω.

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance MeasureTheory.LevyProkhorov.instPseudoMetricSpaceFiniteMeasure {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] : PseudoMetricSpace (LevyProkhorov (FiniteMeasure Ω))

The Lévy-Prokhorov distance levyProkhorovDist makes FiniteMeasure Ω a pseudometric space. The instance is recorded on the type synonym LevyProkhorov (FiniteMeasure Ω) := FiniteMeasure Ω.

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance MeasureTheory.LevyProkhorov.instPseudoMetricSpaceProbabilityMeasure {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] : PseudoMetricSpace (LevyProkhorov (ProbabilityMeasure Ω))

The Lévy-Prokhorov distance levyProkhorovDist makes ProbabilityMeasure Ω a pseudometric space. The instance is recorded on the type synonym LevyProkhorov (ProbabilityMeasure Ω) := ProbabilityMeasure Ω.

Note: For this pseudometric to give the topology of convergence in distribution, one must furthermore assume that Ω is separable.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.LevyProkhorov.edist_measure_def {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] (μ ν : LevyProkhorov (Measure Ω)) : edist μ ν = levyProkhorovEDist μ.toMeasure ν.toMeasure

theorem MeasureTheory.LevyProkhorov.edist_finiteMeasure_def {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] (μ ν : LevyProkhorov (FiniteMeasure Ω)) : edist μ ν = levyProkhorovEDist ↑μ.toMeasure ↑ν.toMeasure

theorem MeasureTheory.LevyProkhorov.dist_finiteMeasure_def {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] (μ ν : LevyProkhorov (FiniteMeasure Ω)) : dist μ ν = levyProkhorovDist ↑μ.toMeasure ↑ν.toMeasure

theorem MeasureTheory.LevyProkhorov.edist_probabilityMeasure_def {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] (μ ν : LevyProkhorov (ProbabilityMeasure Ω)) : edist μ ν = levyProkhorovEDist ↑μ.toMeasure ↑ν.toMeasure

theorem MeasureTheory.LevyProkhorov.dist_probabilityMeasure_def {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] (μ ν : LevyProkhorov (ProbabilityMeasure Ω)) : dist μ ν = levyProkhorovDist ↑μ.toMeasure ↑ν.toMeasure

@[deprecated MeasureTheory.LevyProkhorov.dist_probabilityMeasure_def (since := "2025-10-28")]

theorem MeasureTheory.LevyProkhorov.dist_def {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] (μ ν : LevyProkhorov (ProbabilityMeasure Ω)) : dist μ ν = levyProkhorovDist ↑μ.toMeasure ↑ν.toMeasure

Alias of MeasureTheory.LevyProkhorov.dist_probabilityMeasure_def.

noncomputable instance MeasureTheory.LevyProkhorov.levyProkhorovDist_metricSpace_probabilityMeasure {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] [BorelSpace Ω] : MetricSpace (LevyProkhorov (ProbabilityMeasure Ω))

If Ω is a Borel space, then the Lévy-Prokhorov distance levyProkhorovDist makes ProbabilityMeasure Ω into 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.

Equations

• One or more equations did not get rendered due to their size.

The Lévy-Prokhorov topology is at least as fine as convergence in distribution

theorem MeasureTheory.BoundedContinuousFunction.integral_eq_integral_meas_le_of_hasFiniteIntegral {α : Type u_2} [MeasurableSpace α] [TopologicalSpace α] [OpensMeasurableSpace α] (f : BoundedContinuousFunction α ℝ) (μ : Measure α) (f_nn : 0 ≤ᶠ[ae μ] ⇑f) (hf : HasFiniteIntegral (⇑f) μ) : ∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Set.Ioc 0 ‖f‖, μ.real {a : α | t ≤ f a}

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 MeasureTheory.BoundedContinuousFunction.integral_eq_integral_meas_le {α : Type u_2} [MeasurableSpace α] [TopologicalSpace α] [OpensMeasurableSpace α] (f : BoundedContinuousFunction α ℝ) (μ : Measure α) [IsFiniteMeasure μ] (f_nn : 0 ≤ᶠ[ae μ] ⇑f) : ∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Set.Ioc 0 ‖f‖, μ.real {a : α | t ≤ f a}

A version of the layer cake formula for bounded continuous functions and finite measures: ∫ f dμ = ∫ t in (0, ‖f‖], μ {x | f(x) ≥ t} dt.

theorem MeasureTheory.BoundedContinuousFunction.integral_le_of_levyProkhorovEDist_lt {Ω : Type u_1} [MeasurableSpace Ω] [PseudoMetricSpace Ω] [OpensMeasurableSpace Ω] (μ ν : Measure Ω) [IsFiniteMeasure μ] [IsFiniteMeasure ν] {ε : ℝ} (ε_pos : 0 < ε) (hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε) (f : BoundedContinuousFunction Ω ℝ) (f_nn : 0 ≤ᶠ[ae μ] ⇑f) : ∫ (ω : Ω), f ω ∂μ ≤ (∫ (t : ℝ) in Set.Ioc 0 ‖f‖, ν.real (Metric.thickening ε {a : Ω | t ≤ f a})) + ε * ‖f‖

Assuming levyProkhorovEDist μ ν < ε, we can bound ∫ f ∂μ in terms of ∫ t in (0, ‖f‖], ν (thickening ε {x | f(x) ≥ t}) dt and ‖f‖.

theorem MeasureTheory.tendsto_integral_meas_thickening_le {Ω : Type u_1} [MeasurableSpace Ω] [PseudoMetricSpace Ω] [OpensMeasurableSpace Ω] (f : BoundedContinuousFunction Ω ℝ) {A : Set ℝ} (A_finmeas : volume A ≠ ⊤) (μ : ProbabilityMeasure Ω) : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in A, (↑μ).real (Metric.thickening ε {a : Ω | t ≤ f a})) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (t : ℝ) in A, (↑μ).real {a : Ω | t ≤ f a}))

A monotone decreasing convergence lemma for integrals of measures of thickenings: ∫ t in (0, ‖f‖], μ (thickening ε {x | f(x) ≥ t}) dt tends to ∫ t in (0, ‖f‖], μ {x | f(x) ≥ t} dt as ε → 0.

theorem MeasureTheory.LevyProkhorov.continuous_toMeasure_probabilityMeasure {Ω : Type u_1} [MeasurableSpace Ω] [PseudoMetricSpace Ω] [OpensMeasurableSpace Ω] : Continuous toMeasure

The identity map LevyProkhorov (ProbabilityMeasure Ω) → ProbabilityMeasure Ω is continuous.

@[deprecated MeasureTheory.LevyProkhorov.continuous_toMeasure_probabilityMeasure (since := "2025-10-28")]

theorem MeasureTheory.LevyProkhorov.continuous_equiv_probabilityMeasure {Ω : Type u_1} [MeasurableSpace Ω] [PseudoMetricSpace Ω] [OpensMeasurableSpace Ω] : Continuous toMeasure

Alias of MeasureTheory.LevyProkhorov.continuous_toMeasure_probabilityMeasure.

---

The identity map LevyProkhorov (ProbabilityMeasure Ω) → ProbabilityMeasure Ω is continuous.

theorem MeasureTheory.LevyProkhorov.le_convergenceInDistribution {Ω : Type u_1} [MeasurableSpace Ω] [PseudoMetricSpace Ω] [OpensMeasurableSpace Ω] : TopologicalSpace.coinduced toMeasure inferInstance ≤ inferInstance

The topology of the Lévy-Prokhorov metric is at least as fine as the topology of convergence in distribution.

@[deprecated MeasureTheory.LevyProkhorov.le_convergenceInDistribution (since := "2025-10-28")]

theorem MeasureTheory.levyProkhorov_le_convergenceInDistribution {Ω : Type u_1} [MeasurableSpace Ω] [PseudoMetricSpace Ω] [OpensMeasurableSpace Ω] : TopologicalSpace.coinduced LevyProkhorov.toMeasure inferInstance ≤ inferInstance

Alias of MeasureTheory.LevyProkhorov.le_convergenceInDistribution.

---

The topology of the Lévy-Prokhorov metric is at least as fine as the topology of convergence in distribution.

On separable spaces the Lévy-Prokhorov distance metrizes convergence in distribution

theorem MeasureTheory.ProbabilityMeasure.toMeasure_add_pos_gt_mem_nhds {Ω : Type u_1} [PseudoMetricSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] (P : ProbabilityMeasure Ω) {G : Set Ω} (G_open : IsOpen G) {ε : ENNReal} (ε_pos : 0 < ε) : {Q : ProbabilityMeasure Ω | ↑P G < ↑Q G + ε} ∈ nhds P

theorem MeasureTheory.SeparableSpace.exists_measurable_partition_diam_le (Ω : Type u_1) [PseudoMetricSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] [TopologicalSpace.SeparableSpace Ω] {ε : ℝ} (ε_pos : 0 < ε) : ∃ (As : ℕ → Set Ω), (∀ (n : ℕ), MeasurableSet (As n)) ∧ (∀ (n : ℕ), Bornology.IsBounded (As n)) ∧ (∀ (n : ℕ), Metric.diam (As n) ≤ ε) ∧ ⋃ (n : ℕ), As n = Set.univ ∧ Pairwise fun (n m : ℕ) => Disjoint (As n) (As m)

In a separable pseudometric space, for any ε > 0 there exists a countable collection of disjoint Borel measurable subsets of diameter at most ε that cover the whole space.

theorem MeasureTheory.LevyProkhorov.continuous_ofMeasure_probabilityMeasure {Ω : Type u_1} [PseudoMetricSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] [TopologicalSpace.SeparableSpace Ω] : Continuous ofMeasure

@[deprecated MeasureTheory.LevyProkhorov.continuous_ofMeasure_probabilityMeasure (since := "2025-10-28")]

theorem MeasureTheory.LevyProkhorov.continuous_equiv_symm_probabilityMeasure {Ω : Type u_1} [PseudoMetricSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] [TopologicalSpace.SeparableSpace Ω] : Continuous ofMeasure

Alias of MeasureTheory.LevyProkhorov.continuous_ofMeasure_probabilityMeasure.

theorem MeasureTheory.LevyProkhorov.eq_convergenceInDistribution {Ω : Type u_1} [PseudoMetricSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] [TopologicalSpace.SeparableSpace Ω] : inferInstance = TopologicalSpace.coinduced toMeasure inferInstance

The topology of the Lévy-Prokhorov metric on probability measures on a separable space coincides with the topology of convergence in distribution.

@[deprecated MeasureTheory.LevyProkhorov.eq_convergenceInDistribution (since := "2025-10-28")]

theorem MeasureTheory.levyProkhorov_eq_convergenceInDistribution {Ω : Type u_1} [PseudoMetricSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] [TopologicalSpace.SeparableSpace Ω] : inferInstance = TopologicalSpace.coinduced LevyProkhorov.toMeasure inferInstance

Alias of MeasureTheory.LevyProkhorov.eq_convergenceInDistribution.

---

The topology of the Lévy-Prokhorov metric on probability measures on a separable space coincides with the topology of convergence in distribution.

noncomputable def MeasureTheory.LevyProkhorov.probabilityMeasureHomeomorph {Ω : Type u_1} [PseudoMetricSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] [TopologicalSpace.SeparableSpace Ω] : ProbabilityMeasure Ω ≃ₜ LevyProkhorov (ProbabilityMeasure Ω)

The identity map is a homeomorphism from ProbabilityMeasure Ω with the topology of convergence in distribution to ProbabilityMeasure Ω with the Lévy-Prokhorov (pseudo)metric.

Equations

• One or more equations did not get rendered due to their size.

@[deprecated MeasureTheory.LevyProkhorov.probabilityMeasureHomeomorph (since := "2025-10-28")]

def MeasureTheory.homeomorph_probabilityMeasure_levyProkhorov {Ω : Type u_1} [PseudoMetricSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] [TopologicalSpace.SeparableSpace Ω] : ProbabilityMeasure Ω ≃ₜ LevyProkhorov (ProbabilityMeasure Ω)

Alias of MeasureTheory.LevyProkhorov.probabilityMeasureHomeomorph.

---

The identity map is a homeomorphism from ProbabilityMeasure Ω with the topology of convergence in distribution to ProbabilityMeasure Ω with the Lévy-Prokhorov (pseudo)metric.

Equations

• @MeasureTheory.homeomorph_probabilityMeasure_levyProkhorov = @MeasureTheory.LevyProkhorov.probabilityMeasureHomeomorph

instance MeasureTheory.instPseudoMetrizableSpaceProbabilityMeasureOfSeparableSpace (X : Type u_2) [TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] [TopologicalSpace.SeparableSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] : TopologicalSpace.PseudoMetrizableSpace (ProbabilityMeasure X)

The topology of convergence in distribution on a separable space is pseudo-metrizable.

instance MeasureTheory.instMetrizableSpaceProbabilityMeasure (X : Type u_2) [TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] [TopologicalSpace.SeparableSpace X] [MeasurableSpace X] [BorelSpace X] : TopologicalSpace.MetrizableSpace (ProbabilityMeasure X)

The topology of convergence in distribution on a separable Borel space is metrizable.