Theorems · Definition · probability

MeasureTheory.levyProkhorovEDist

{Ω : Type u_1} →
  [inst : 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}.

Defined in

Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Cited by

20 results in Mathlib

Foundations

Depth 170 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpacePseudoEMetricSpace