Theorems · Theorem · probability

MeasureTheory.levyProkhorovEDist_le_of_forall_add_pos_le

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

Defined in

Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpacePseudoEMetricSpace