Theorems · Theorem · measure theory

MeasureTheory.measureReal_abs_dual_gt_le_integral_charFunDual

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mE : MeasurableSpace E}
  [OpensMeasurableSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure μ] (L : StrongDual ℝ E)
  {r : ℝ},
  0 < r → μ.real {x | r < |L x|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - MeasureTheory.charFunDual μ (t • L)‖

For a probability measure on a normed space E and L : Dual ℝ E, a bound on the measure of the set {x | r < |L x|} in terms of the integral of the characteristic function.

Defined in

Mathlib.MeasureTheory.Measure.IntegralCharFun

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceOpensMeasurableSpaceMeasureTheory.IsProbabilityMeasure