English
For y ≥ z and a nonnegative function f, the integral over (−∞, y] equals the sum of the integrals over (−∞, z) and [z, y].
Русский
Для y ≥ z и неотрицательной функции f интеграл по (−∞, y] равен сумме интегралов по (−∞, z) и [z, y].
LaTeX
$$$\\int_{(-\\infty, y]} f = \\int_{(-\\infty, z)} f + \\int_{[z, y]} f \\quad (f:\\mathbb{R}\\to \\mathbb{R}_{\\ge 0})$$$
Lean4
/-- For `μ` a probability measure whose product with itself is invariant by rotation and for `a, c`
with `2⁻¹ < c ≤ μ {x | ‖x‖ ≤ a}`, the integral `∫⁻ x, exp (logRatio c * a⁻¹ ^ 2 * ‖x‖ ^ 2) ∂μ`
is bounded by a quantity that does not depend on `a`. -/
theorem lintegral_exp_mul_sq_norm_le_of_map_rotation_eq_self [IsProbabilityMeasure μ]
(h_rot : (μ.prod μ).map (ContinuousLinearMap.rotation (-(π / 4))) = μ.prod μ) {c : ℝ≥0∞} (hc : c ≤ μ {x | ‖x‖ ≤ a})
(hc_gt : 2⁻¹ < c) :
∫⁻ x, .ofReal (rexp (logRatio c * a⁻¹ ^ 2 * ‖x‖ ^ 2)) ∂μ ≤
.ofReal (rexp (logRatio c)) + ∑' n, .ofReal (rexp (-2⁻¹ * Real.log (c / (1 - c)).toReal * 2 ^ n)) :=
by
by_cases ha : a = 0
· simp only [ha, inv_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, mul_zero, zero_mul, Real.exp_zero,
ENNReal.ofReal_one, lintegral_const, measure_univ, mul_one, ENNReal.toReal_div, neg_mul]
refine le_add_right ?_
rw [← ENNReal.ofReal_one]
gcongr
simp only [Real.one_le_exp_iff]
exact logRatio_nonneg hc_gt.le (hc.trans prob_le_one)
have ha_pos : 0 < a := by
refine lt_of_le_of_ne' ?_ ha
by_contra h_neg
have : {x : E | ‖x‖ ≤ a} = ∅ := by
ext x
simp only [Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false, not_le]
exact (not_le.mp h_neg).trans_le (norm_nonneg _)
simp only [this, measure_empty, nonpos_iff_eq_zero] at hc
simp [hc] at hc_gt
refine (lintegral_exp_mul_sq_norm_le_mul h_rot ha_pos hc hc_gt).trans ?_
conv_rhs => rw [← one_mul (ENNReal.ofReal _ + _)]
gcongr
exact prob_le_one
