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.
• 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.

TODO

• Show that in Borel spaces, the Lévy-Prokhorov distance is a metric; not just a pseudometric.

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 μ ν ≤ δ

A general sufficient condition for bounding levyProkhorovEDist from above.

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 μ ν ≤ δ

A simple general sufficient condition for bounding levyProkhorovEDist from above.

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 ↑μ ↑ν

theorem MeasureTheory.levyProkhorovEDist_le_of_forall_le {Ω : Type u_2} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (ν : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (δ : ENNReal) (h : ∀ (ε : ENNReal) (B : Set Ω), δ < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (Metric.thickening ε.toReal B) + ε) : MeasureTheory.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_2} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (ν : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {δ : ℝ} (δ_nn : 0 ≤ δ) (h : ∀ (ε : ℝ) (B : Set Ω), δ < ε → MeasurableSet B → μ B ≤ ν (Metric.thickening ε B) + ENNReal.ofReal ε) : MeasureTheory.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.

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

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

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

Equations

• μ.toProbabilityMeasure = μ

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

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

Equations

• μ.toLevyProkhorov = μ

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

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

Equations

• μ.finiteMeasure = μ

theorem MeasureTheory.BoundedContinuousFunction.integral_eq_integral_meas_le_of_hasFiniteIntegral {α : Type u_3} [MeasurableSpace α] [TopologicalSpace α] [OpensMeasurableSpace α] (f : BoundedContinuousFunction α ℝ) (μ : MeasureTheory.Measure α) (f_nn : 0 ≤ᵐ[μ] ⇑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 ≤ᵐ[μ] ⇑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 ≤ᵐ[μ] ⇑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, (↑(μ (Metric.thickening ε {a : Ω | t ≤ f a}))).toReal) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (t : ℝ) in A, (↑(μ {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.LevyProkhorov.continuous_toProbabilityMeasure {Ω : Type u_2} [MeasurableSpace Ω] [PseudoMetricSpace Ω] [OpensMeasurableSpace Ω] : Continuous MeasureTheory.LevyProkhorov.toProbabilityMeasure

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

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

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.SeparableSpace.exists_measurable_partition_diam_le (Ω : Type u_2) [PseudoMetricSpace Ω] [TopologicalSpace.SeparableSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] {ε : ℝ} (ε_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.ProbabilityMeasure.toMeasure_add_pos_gt_mem_nhds {Ω : Type u_2} [PseudoMetricSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] (P : MeasureTheory.ProbabilityMeasure Ω) {G : Set Ω} (G_open : IsOpen G) {ε : ENNReal} (ε_pos : 0 < ε) : {Q : MeasureTheory.ProbabilityMeasure Ω | ↑P G < ↑Q G + ε} ∈ nhds P

theorem MeasureTheory.ProbabilityMeasure.continuous_toLevyProkhorov {Ω : Type u_2} [PseudoMetricSpace Ω] [TopologicalSpace.SeparableSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] : Continuous MeasureTheory.ProbabilityMeasure.toLevyProkhorov

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

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

def MeasureTheory.homeomorph_probabilityMeasure_levyProkhorov {Ω : Type u_2} [PseudoMetricSpace Ω] [TopologicalSpace.SeparableSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] : MeasureTheory.ProbabilityMeasure Ω ≃ₜ MeasureTheory.LevyProkhorov (MeasureTheory.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.

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

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

Equations

• ⋯ = ⋯