Theorems · Theorem · probability

MeasureTheory.BoundedContinuousFunction.integral_le_of_levyProkhorovEDist_lt

∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoMetricSpace Ω] [OpensMeasurableSpace Ω]
  (μ ν : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {ε : ℝ},
  0 < ε →
    MeasureTheory.levyProkhorovEDist μ ν < ENNReal.ofReal ε →
      ∀ (f : BoundedContinuousFunction Ω ℝ),
        0 ≤ᵐ[μ] ⇑f →
          ∫ (ω : Ω), f ω ∂μ ≤ (∫ (t : ℝ) in Set.Ioc 0 ‖f‖, ν.real (Metric.thickening ε {a | t ≤ f a})) + ε * ‖f‖

Assuming levyProkhorovEDist μ ν < ε, we can bound ∫ f ∂μ in terms of ∫ t in (0, ‖f‖], ν (thickening ε {x | f(x) ≥ t}) dt and ‖f‖.

Defined in

Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpacePseudoMetricSpaceOpensMeasurableSpaceMeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasure