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 Ω] [PseudoEMetricSpace Ω] (μ : 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 Ω] [PseudoEMetricSpace Ω] {ε₁ : 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 Ω] [PseudoEMetricSpace Ω] {μ : 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 Ω] [PseudoEMetricSpace Ω] {μ : 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 Ω] [PseudoEMetricSpace Ω] (μ : 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 Ω] [PseudoEMetricSpace Ω] (μ : 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 Ω] [PseudoEMetricSpace Ω] (μ : MeasureTheory.Measure Ω) (ν : MeasureTheory.Measure Ω) : MeasureTheory.levyProkhorovEDist μ ν ≤ max (↑↑μ Set.univ) (↑↑ν Set.univ)

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

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

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

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

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

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

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

theorem MeasureTheory.levyProkhorovDist_triangle {Ω : Type u_2} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [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 Ω] [PseudoEMetricSpace Ω] [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 Ω] [PseudoEMetricSpace Ω] [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 Ω] [PseudoEMetricSpace Ω] [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.

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

def MeasureTheory.LevyProkhorov.probabilityMeasure {Ω : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.LevyProkhorov (MeasureTheory.ProbabilityMeasure Ω)) : MeasureTheory.ProbabilityMeasure Ω

Coercion from the type synonym LevyProkhorov (ProbabilityMeasure Ω) to ProbabilityMeasure Ω.

Equations

• MeasureTheory.LevyProkhorov.probabilityMeasure μ = μ

def MeasureTheory.LevyProkhorov.finiteMeasure {Ω : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.LevyProkhorov (MeasureTheory.FiniteMeasure Ω)) : MeasureTheory.FiniteMeasure Ω

Coercion from the type synonym LevyProkhorov (FiniteMeasure Ω) to FiniteMeasure Ω.

Equations

• MeasureTheory.LevyProkhorov.finiteMeasure μ = μ

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

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

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_2} [MeasurableSpace Ω] [PseudoMetricSpace Ω] [OpensMeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (ν : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {ε : ℝ} (ε_pos : 0 < ε) (hμν : MeasureTheory.levyProkhorovEDist μ ν < ENNReal.ofReal ε) (f : BoundedContinuousFunction Ω ℝ) (f_nn : 0 ≤ᶠ[MeasureTheory.Measure.ae μ] ⇑f) : ∫ (ω : Ω), f ω ∂μ ≤ (∫ (t : ℝ) in Set.Ioc 0 ‖f‖, (↑↑ν (Metric.thickening ε {a : Ω | t ≤ f a})).toReal) + ε * ‖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_2} [MeasurableSpace Ω] [PseudoMetricSpace Ω] [OpensMeasurableSpace Ω] (f : BoundedContinuousFunction Ω ℝ) {A : Set ℝ} (A_finmeas : ↑↑MeasureTheory.volume A ≠ ⊤) (μ : MeasureTheory.ProbabilityMeasure Ω) : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in A, (↑((fun (s : Set Ω) => (↑↑↑μ s).toNNReal) (Metric.thickening ε {a : Ω | t ≤ f a}))).toReal) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (t : ℝ) in A, (↑((fun (s : Set Ω) => (↑↑↑μ s).toNNReal) {a : Ω | t ≤ f a})).toReal))

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.continuous_levyProkhorov_to_probabilityMeasure {Ω : Type u_2} [MeasurableSpace Ω] [PseudoMetricSpace Ω] [OpensMeasurableSpace Ω] : Continuous MeasureTheory.LevyProkhorov.probabilityMeasure

The coercion LevyProkhorov (ProbabilityMeasure Ω) → ProbabilityMeasure Ω is continuous.

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

The topology of the Lévy-Prokhorov metric is finer than the topology of convergence in distribution.