Theorems · Theorem · measure theory

MeasureTheory.measureReal_abs_gt_le_integral_charFun

∀ {μ : MeasureTheory.Measure ℝ} {r : ℝ} [MeasureTheory.IsProbabilityMeasure μ],
  0 < r → μ.real {x | r < |x|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - MeasureTheory.charFun μ t‖

A bound on the measure of the set {x | r < |x|} in terms of the integral of the characteristic function, for a probability measure on ℝ.

Defined in

Mathlib.MeasureTheory.Measure.IntegralCharFun

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsProbabilityMeasure