English
For c > 1/2, c < 1 and any n, we have logRatio(c) · normThreshold(a,n+1)^2 · a^(-2) ≤ (1/2) log(c/(1-c)) · 2^n.
Русский
Для c > 1/2, c < 1 и любого n выполняется: logRatio(c) · normThreshold(a,n+1)^2 · a^(-2) ≤ (1/2) log(c/(1-c)) · 2^n.
LaTeX
$$\\text{If } (2)^{-1} < c < 1, \\quad logRatio(c) \\cdot (\\operatorname{normThreshold}(a,n+1))^{2} \\cdot a^{-2} \\le \\tfrac12 \\log\\left(\\dfrac{c}{1-c}\\right) \\cdot 2^{n}$$
Lean4
/-- Auxiliary lemma for `lintegral_exp_mul_sq_norm_le_mul`, in which we find an upper bound on an
integral by dealing separately with the contribution of each set in a sequence of annuli.
This is the bound of the integral over one of those annuli. -/
theorem lintegral_closedBall_diff_exp_logRatio_mul_sq_le [IsProbabilityMeasure μ]
(h_rot : (μ.prod μ).map (ContinuousLinearMap.rotation (-(π / 4))) = μ.prod μ) (ha_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a})
(ha_lt : μ {x | ‖x‖ ≤ a} < 1) (n : ℕ) :
∫⁻ x in (closedBall 0 (normThreshold a (n + 1)) \ closedBall 0 (normThreshold a n)),
.ofReal (rexp (logRatio (μ {x | ‖x‖ ≤ a}) * a⁻¹ ^ 2 * ‖x‖ ^ 2)) ∂μ ≤
μ {x | ‖x‖ ≤ a} * .ofReal (rexp (-2⁻¹ * Real.log (μ {x | ‖x‖ ≤ a} / (1 - μ {x | ‖x‖ ≤ a})).toReal * 2 ^ n)) :=
let t := normThreshold a
let c := μ {x | ‖x‖ ≤ a}
let C := logRatio c * a⁻¹ ^ 2
calc
∫⁻ x in (closedBall 0 (t (n + 1)) \ closedBall 0 (t n)), .ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ
_ ≤ ∫⁻ x in (closedBall 0 (t (n + 1)) \ closedBall 0 (t n)), .ofReal (rexp (C * t (n + 1) ^ 2)) ∂μ :=
by
refine setLIntegral_mono (by fun_prop) fun x hx ↦ ?_
gcongr
· exact mul_nonneg (logRatio_pos ha_gt ha_lt).le (by positivity)
· simp only [Set.mem_diff, mem_closedBall, dist_zero_right, not_le] at hx
exact
hx.1
-- The integral of a constant is the constant times the measure of the set
_ = .ofReal (rexp (C * t (n + 1) ^ 2)) * μ (closedBall 0 (t (n + 1)) \ closedBall 0 (t n)) := by
simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter, C, t]
_ ≤ .ofReal (rexp (C * t (n + 1) ^ 2)) * μ {x | t n < ‖x‖} :=
by
gcongr
intro x
simp
-- We obtained an upper bound on the measure of that annulus in a previous lemma
_ ≤ .ofReal (rexp (C * t (n + 1) ^ 2)) * c * .ofReal (rexp (-Real.log (c / (1 - c)).toReal * 2 ^ n)) :=
by
conv_rhs => rw [mul_assoc]
gcongr
exact measure_gt_normThreshold_le_exp h_rot ha_gt ha_lt n
_ ≤
.ofReal (rexp (2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * 2 ^ n)) * c *
.ofReal (rexp (-Real.log (c / (1 - c)).toReal * 2 ^ n)) :=
by
gcongr ENNReal.ofReal (rexp ?_) * _ * _
convert logRatio_mul_normThreshold_add_one_le ha_gt ha_lt n (a := a) using 1
ring
_ = c * .ofReal (rexp (-2⁻¹ * Real.log (c / (1 - c)).toReal * 2 ^ n)) :=
by
rw [mul_comm _ c, mul_assoc, ← ENNReal.ofReal_mul (by positivity), ← Real.exp_add]
congr
norm_cast
simp only [Nat.cast_pow, Nat.cast_ofNat, ENNReal.toReal_div, neg_mul]
field_simp
ring
