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.

Tags

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

Lévy-Prokhorov metric

noncomputable def MeasureTheory.levyProkhorovEDist {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] (μ ν : 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_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] {ε₁ ε₂ : ENNReal} (μ ν : 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_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] {μ ν : 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_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] {μ ν : 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_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] (μ ν : 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_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] (μ ν : 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_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] (μ ν : MeasureTheory.Measure Ω) : MeasureTheory.levyProkhorovEDist μ ν ≤ μ Set.univ ⊔ ν Set.univ

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

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

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

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

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

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

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

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

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

Equations

• MeasureTheory.LevyProkhorov α = α

def MeasureTheory.LevyProkhorov.equiv (α : Type u_2) : MeasureTheory.LevyProkhorov α ≃ α

The "identity" equivalence between the type synonym LevyProkhorov α and α.

Equations

• MeasureTheory.LevyProkhorov.equiv α = Equiv.refl (MeasureTheory.LevyProkhorov α)

noncomputable instance MeasureTheory.instPseudoEMetricSpaceLevyProkhorovMeasure {Ω : Type u_1} [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_1} [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.

theorem MeasureTheory.measure_le_measure_closure_of_levyProkhorovEDist_eq_zero {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] {μ ν : MeasureTheory.Measure Ω} (hLP : MeasureTheory.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 Ω] {μ ν : MeasureTheory.Measure Ω} (hLP : MeasureTheory.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.

noncomputable instance MeasureTheory.levyProkhorovDist_pseudoMetricSpace_probabilityMeasure {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] : PseudoMetricSpace (MeasureTheory.LevyProkhorov (MeasureTheory.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.dist_def {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] (μ ν : MeasureTheory.LevyProkhorov (MeasureTheory.ProbabilityMeasure Ω)) : dist μ ν = MeasureTheory.levyProkhorovDist ↑μ ↑ν

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

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.

Equations

• MeasureTheory.levyProkhorovDist_metricSpace_probabilityMeasure = MetricSpace.mk ⋯

theorem MeasureTheory.levyProkhorovEDist_le_of_forall_le {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] (μ ν : 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_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] (μ ν : 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

theorem MeasureTheory.BoundedContinuousFunction.integral_eq_integral_meas_le_of_hasFiniteIntegral {α : Type u_2} [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_2} [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_1} [MeasurableSpace Ω] [PseudoMetricSpace Ω] [OpensMeasurableSpace Ω] (μ ν : 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_1} [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_equiv_probabilityMeasure {Ω : Type u_1} [MeasurableSpace Ω] [PseudoMetricSpace Ω] [OpensMeasurableSpace Ω] : Continuous ⇑(MeasureTheory.LevyProkhorov.equiv (MeasureTheory.ProbabilityMeasure Ω))

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

theorem MeasureTheory.levyProkhorov_le_convergenceInDistribution {Ω : Type u_1} [MeasurableSpace Ω] [PseudoMetricSpace Ω] [OpensMeasurableSpace Ω] : TopologicalSpace.coinduced (⇑(MeasureTheory.LevyProkhorov.equiv (MeasureTheory.ProbabilityMeasure Ω))) 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.ProbabilityMeasure.toMeasure_add_pos_gt_mem_nhds {Ω : Type u_1} [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.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_equiv_symm_probabilityMeasure {Ω : Type u_1} [PseudoMetricSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] [TopologicalSpace.SeparableSpace Ω] : Continuous ⇑(MeasureTheory.LevyProkhorov.equiv (MeasureTheory.ProbabilityMeasure Ω)).symm

theorem MeasureTheory.levyProkhorov_eq_convergenceInDistribution {Ω : Type u_1} [PseudoMetricSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] [TopologicalSpace.SeparableSpace Ω] : inferInstance = TopologicalSpace.coinduced (⇑(MeasureTheory.LevyProkhorov.equiv (MeasureTheory.ProbabilityMeasure Ω))) 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_1} [PseudoMetricSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] [TopologicalSpace.SeparableSpace Ω] : 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_2) [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

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯