English
For a probability measure μ on a normed space E and a continuous linear functional L in the dual, the μ-real measure of {x : r < |L(x)|} is bounded by a constant times the L1-norm of 1 - charFunDual μ (t · L) over a symmetric interval: μ.real({x : r < |L x|}) ≤ (1/2) r || ∫ t in -2/r .. 2/r, 1 - charFunDual μ (t · L) ||.
Русский
Для вероятностной меры μ на нормационном пространстве E и линейного функционала L в двойственном пространстве, неравенство: μ.real({x: r < |L(x)|}) ≤ (1/2) r || ∫ ... ||.
LaTeX
$$$\mu\_{\mathbb{R}}(\{x:\, r<|L x|\}) \leq \tfrac12 r \left\| \int_{-2/r}^{2/r} (1 - \operatorname{charFun}_{\mathcal{D}}(t L)) \, dt \right\|$$$
Lean4
/-- 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 measureReal_abs_dual_gt_le_integral_charFunDual {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
{mE : MeasurableSpace E} [OpensMeasurableSpace E] {μ : Measure E} [IsProbabilityMeasure μ] (L : StrongDual ℝ E)
{r : ℝ} (hr : 0 < r) : μ.real {x | r < |L x|} ≤ 2⁻¹ * r * ‖∫ t in -2 * r⁻¹..2 * r⁻¹, 1 - charFunDual μ (t • L)‖ :=
by
have : IsProbabilityMeasure (μ.map L) := Measure.isProbabilityMeasure_map (by fun_prop)
convert measureReal_abs_gt_le_integral_charFun (μ := μ.map L) hr with x
· rw [map_measureReal_apply (by fun_prop)]
· simp
· exact MeasurableSet.preimage measurableSet_Ioi (by fun_prop)
· rw [charFun_map_eq_charFunDual_smul]
