Theorems · Theorem · probability

MeasureTheory.levyProkhorovEDist_le_of_forall_le

∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω]
  (μ ν : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν]
  (δ : ENNReal),
  (∀ (ε : 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.

Defined in

Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpacePseudoEMetricSpaceOpensMeasurableSpaceMeasureTheory.IsProbabilityMeasureMeasureTheory.IsProbabilityMeasure