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

• levyProkhorovDist_pseudoMetricSpace_finiteMeasure: The Lévy-Prokhorov distance is a pseudoemetric on the space of finite measures.
• levyProkhorovDist_pseudoMetricSpace_probabilityMeasure: The Lévy-Prokhorov distance is a pseudoemetric on the space of probability measures.

Todo

• Show that in Borel spaces, the Lévy-Prokhorov distance is a metric; not just a pseudometric.
• Prove that if X is metrizable and separable, then the Lévy-Prokhorov distance metrizes the topology of weak convergence.

Tags

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

Lévy-Prokhorov metric

noncomputable def MeasureTheory.levyProkhorovEDist {Ω : Type u_2} [MeasurableSpace Ω] [MetricSpace Ω] (μ : MeasureTheory.Measure Ω) (ν : MeasureTheory.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_2} [MeasurableSpace Ω] [MetricSpace Ω] {ε₁ : ENNReal} {ε₂ : ENNReal} (μ : MeasureTheory.Measure Ω) (ν : MeasureTheory.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_2} [MeasurableSpace Ω] [MetricSpace Ω] {μ : MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω} {c : ENNReal} (h : MeasureTheory.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_2} [MeasurableSpace Ω] [MetricSpace Ω] {μ : MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω} {c : ENNReal} (h : MeasureTheory.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_2} [MeasurableSpace Ω] [MetricSpace Ω] (μ : MeasureTheory.Measure Ω) (ν : MeasureTheory.Measure Ω) (δ : ENNReal) (h : ∀ (ε : ENNReal) (B : Set Ω), 0 < ε → ε < ⊤ → MeasurableSet B → ↑↑μ B ≤ ↑↑ν (Metric.thickening (δ + ε).toReal B) + δ + ε ∧ ↑↑ν B ≤ ↑↑μ (Metric.thickening (δ + ε).toReal B) + δ + ε) : MeasureTheory.levyProkhorovEDist μ ν ≤ δ

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

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

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

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

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

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

noncomputable def MeasureTheory.levyProkhorovDist {Ω : Type u_2} [MeasurableSpace Ω] [MetricSpace Ω] (μ : MeasureTheory.Measure Ω) (ν : MeasureTheory.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_2} [MeasurableSpace Ω] [MetricSpace Ω] (μ : MeasureTheory.Measure Ω) : MeasureTheory.levyProkhorovDist μ μ = 0

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

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

def MeasureTheory.LevyProkhorov (α : Type u_3) : Type u_3

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

Equations

• MeasureTheory.LevyProkhorov α = α

noncomputable instance MeasureTheory.instPseudoEMetricSpaceLevyProkhorovMeasure {Ω : Type u_2} [MeasurableSpace Ω] [MetricSpace Ω] [OpensMeasurableSpace Ω] : PseudoEMetricSpace (MeasureTheory.LevyProkhorov (MeasureTheory.Measure Ω))

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

Equations

• MeasureTheory.instPseudoEMetricSpaceLevyProkhorovMeasure = PseudoEMetricSpace.mk ⋯ ⋯ ⋯ (uniformSpaceOfEDist MeasureTheory.levyProkhorovEDist ⋯ ⋯ ⋯) ⋯

noncomputable instance MeasureTheory.levyProkhorovDist_pseudoMetricSpace_finiteMeasure {Ω : Type u_2} [MeasurableSpace Ω] [MetricSpace Ω] [OpensMeasurableSpace Ω] : PseudoMetricSpace (MeasureTheory.LevyProkhorov (MeasureTheory.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.levyProkhorovDist_pseudoMetricSpace_probabilityMeasure {Ω : Type u_2} [MeasurableSpace Ω] [MetricSpace Ω] [OpensMeasurableSpace Ω] : PseudoMetricSpace (MeasureTheory.LevyProkhorov (MeasureTheory.ProbabilityMeasure Ω))

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

Equations

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