Integrals of characteristic functions

This file contains results about integrals of characteristic functions, and lemmas relating the measure of some sets to integrals of characteristic functions.

Main statements

• integral_charFun_Icc: ∫ t in -r..r, charFun μ t = 2 * r * ∫ x, sinc (r * x) ∂μ
• measureReal_abs_gt_le_integral_charFun: bound on the measure of the set {x | r < |x|} in terms of the integral of the characteristic function of μ, for μ a probability measure on ℝ: μ.real {x | r < |x|} ≤ 2⁻¹ * r * ‖∫ t in (-2 * r⁻¹)..(2 * r⁻¹), 1 - charFun μ t‖
• measureReal_abs_dual_gt_le_integral_charFunDual: an application of the previous lemma in a normed space E, which gives for all L : Dual ℝ E, μ.real {x | r < |L x|} ≤ 2⁻¹ * r * ‖∫ t in -2 * r⁻¹..2 * r⁻¹, 1 - charFunDual μ (t • L)‖
• measureReal_abs_inner_gt_le_integral_charFun: an application in an inner product space, which gives for all a, μ.real {x | r < |⟪a, x⟫|} ≤ 2⁻¹ * r * ‖∫ t in -2 * r⁻¹..2 * r⁻¹, 1 - charFun μ (t • a)‖

theorem MeasureTheory.integral_charFun_Icc {μ : Measure ℝ} {r : ℝ} [IsFiniteMeasure μ] (hr : 0 < r) : ∫ (t : ℝ) in -r..r, charFun μ t = 2 * ↑r * ↑(∫ (x : ℝ), Real.sinc (r * x) ∂μ)

theorem MeasureTheory.measureReal_abs_gt_le_integral_charFun {μ : Measure ℝ} {r : ℝ} [IsProbabilityMeasure μ] (hr : 0 < r) : μ.real {x : ℝ | r < |x|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - 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 ℝ.

theorem MeasureTheory.measureReal_abs_dual_gt_le_integral_charFunDual {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} [OpensMeasurableSpace E] {μ : Measure E} [IsProbabilityMeasure μ] (L : NormedSpace.Dual ℝ E) {r : ℝ} (hr : 0 < r) : μ.real {x : E | r < |L x|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - 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.

theorem MeasureTheory.measureReal_abs_inner_gt_le_integral_charFun {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {mE : MeasurableSpace E} [OpensMeasurableSpace E] {μ : Measure E} [IsProbabilityMeasure μ] {a : E} {r : ℝ} (hr : 0 < r) : μ.real {x : E | r < |inner ℝ a x|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun μ (t • a)‖

A bound on the measure of the set {x | r < |⟪a, x⟫|} in terms of the integral of the characteristic function, for a probability measure on an inner product space.