English
For a probability measure μ on the real line and r > 0, the μ-real measure of the set {x : r < |x|} is bounded by a constant times the L1-norm of 1 - charFun μ over a symmetric interval: μ.real({x: r < |x|}) ≤ (1/2) r || ∫_{-2/r}^{2/r} (1 - χ_μ(t)) dt ||.
Русский
Для вероятностной меры μ на прямой справедливо неравенство: μ.real({x: r < |x|}) ≤ (1/2) r || ∫_{-2/r}^{2/r} (1 - χ_μ(t)) dt ||, при r > 0.
LaTeX
$$$\mu\_{\mathbb{R}}(\{x:\, r<|x|\}) \leq \tfrac12 r \left\| \int_{-2/r}^{2/r} (1 - \operatorname{charFun}_{\mu}(t)) \, dt \right\|$$$
Lean4
/-- 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 measureReal_abs_gt_le_integral_charFun [IsProbabilityMeasure μ] (hr : 0 < r) :
μ.real {x | r < |x|} ≤ 2⁻¹ * r * ‖∫ t in (-2 * r⁻¹)..(2 * r⁻¹), 1 - charFun μ t‖ :=
by
have integrable_sinc_const_mul (r : ℝ) : Integrable (fun x ↦ sinc (r * x)) μ :=
(integrable_map_measure stronglyMeasurable_sinc.aestronglyMeasurable (by fun_prop)).mp integrable_sinc
calc
μ.real {x | r < |x|}
_ = μ.real {x | 2 < |2 * r⁻¹ * x|} := by
congr 1 with x
simp only [Set.mem_setOf_eq, abs_mul, Nat.abs_ofNat]
rw [abs_of_nonneg (a := r⁻¹) (by positivity), mul_assoc, ← inv_mul_lt_iff₀ (by positivity),
inv_mul_cancel₀ (by positivity), lt_inv_mul_iff₀ (by positivity), mul_one]
_ = ∫ x in {x | 2 < |2 * r⁻¹ * x|}, 1 ∂μ := by simp
_ = 2 * ∫ x in {x | 2 < |2 * r⁻¹ * x|}, 2⁻¹ ∂μ :=
by
rw [← integral_const_mul]
congr with _
rw [mul_inv_cancel₀ (by positivity)]
_ ≤ 2 * ∫ x in {x | 2 < |2 * r⁻¹ * x|}, 1 - sinc (2 * r⁻¹ * x) ∂μ :=
by
gcongr (2 : ℝ) * ?_
refine
setIntegral_mono_on ?_ ((integrable_const _).sub (integrable_sinc_const_mul _)).integrableOn ?_ fun x hx ↦ ?_
· exact Integrable.integrableOn <| by fun_prop
· exact MeasurableSet.preimage measurableSet_Ioi (by fun_prop)
· have hx_ne : 2 * r⁻¹ * x ≠ 0 := by
intro hx0
simp only [hx0, Set.mem_setOf_eq, abs_zero] at hx
linarith
rw [le_sub_iff_add_le, ← le_sub_iff_add_le']
norm_num
rw [one_div]
refine (sinc_le_inv_abs hx_ne).trans ?_
exact (inv_le_inv₀ (by positivity) (by positivity)).mpr (le_of_lt hx)
_ ≤ 2 * ∫ x, 1 - sinc (2 * r⁻¹ * x) ∂μ :=
by
grw [setIntegral_le_integral (by fun_prop) <| ae_of_all _ fun x ↦ ?_]
simp only [Pi.zero_apply, sub_nonneg]
exact sinc_le_one (2 * r⁻¹ * x)
_ ≤ 2 * ‖∫ x, 1 - sinc (2 * r⁻¹ * x) ∂μ‖ := by
gcongr
exact Real.le_norm_self _
_ = 2⁻¹ * r * ‖2 * (r : ℂ)⁻¹ + 2 * r⁻¹ - 2 * (2 * r⁻¹) * ∫ x, sinc (2 * r⁻¹ * x) ∂μ‖ :=
by
norm_cast
rw [← two_mul, mul_assoc 2, ← mul_sub, norm_mul, Real.norm_ofNat, ← mul_assoc, ← mul_one_sub, norm_mul,
Real.norm_of_nonneg (r := 2 * r⁻¹) (by positivity), ← mul_assoc]
congr
· ring_nf
rw [mul_inv_cancel₀ (by positivity), one_mul]
· rw [integral_sub (integrable_const _) (integrable_sinc_const_mul _)]
simp
_ = 2⁻¹ * r * ‖∫ t in (-2 * r⁻¹)..(2 * r⁻¹), 1 - charFun μ t‖ :=
by
rw [intervalIntegral.integral_sub intervalIntegrable_const intervalIntegrable_charFun, neg_mul,
integral_charFun_Icc (by positivity)]
simp
