English
For a probability measure μ on an inner product space E and a ∈ E, the μ-real measure of {x : r < |⟪a, x⟫|} is bounded by a constant times the L1-norm of 1 - charFun μ (t · a): μ.real({x : r < |⟪a, x⟫|}) ≤ (1/2) r || ∫ t in -2/r..2/r, 1 - χ μ (t a) ||.
Русский
Для вероятностной меры μ на внутренне линейном пространстве E и фиксированного a∈E, имеет место неравенство: μ.real({x: r < |⟪a,x⟫|}) ≤ (1/2) r || ∫ ... ||.
LaTeX
$$$\mu\_{\mathbb{R}}(\{x:\, r<|\langle a,x\rangle|\}) \leq \tfrac12 r \left\| \int_{-2/r}^{2/r} (1 - \operatorname{charFun}_{\mu}(t a)) \, dt \right\|$$$
Lean4
/-- 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. -/
theorem measureReal_abs_inner_gt_le_integral_charFun {E : Type*} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E]
{mE : MeasurableSpace E} [OpensMeasurableSpace E] {μ : Measure E} [IsProbabilityMeasure μ] {a : E} {r : ℝ}
(hr : 0 < r) : μ.real {x | r < |⟪a, x⟫|} ≤ 2⁻¹ * r * ‖∫ t in -2 * r⁻¹..2 * r⁻¹, 1 - charFun μ (t • a)‖ :=
by
have : IsProbabilityMeasure (μ.map (fun x ↦ ⟪a, x⟫)) := Measure.isProbabilityMeasure_map (by fun_prop)
convert measureReal_abs_gt_le_integral_charFun (μ := μ.map (fun x ↦ ⟪a, x⟫)) hr with x
· rw [map_measureReal_apply (by fun_prop)]
· simp
· exact MeasurableSet.preimage measurableSet_Ioi (by fun_prop)
· simp only [charFun_apply, inner_smul_right, conj_trivial, ofReal_mul, RCLike.inner_apply]
rw [integral_map (by fun_prop) (by fun_prop)]
simp_rw [real_inner_comm a]
