English
Let c' ≤ μ({‖x‖ ≤ a}) with 2⁻¹ < c' and μ({‖x‖ ≤ a}) < 1. Then for all n, μ({normThreshold(a,n) < ‖x‖}) ≤ μ({‖x‖ ≤ a}) · exp(-2^n · log(c'/(1−c')).toReal).
Русский
Пусть c' ≤ μ({‖x‖ ≤ a}) и 2⁻¹ < c', а также μ({‖x‖ ≤ a}) < 1. Тогда для всех n выполняется: μ({normThreshold(a,n) < ‖x‖}) ≤ μ({‖x‖ ≤ a}) · exp(-2^n · log(c'/(1−c')).toReal).
LaTeX
$$$\\mu\\{x : \\|x\\| > \\operatorname{normThreshold}(a,n)\\} \\le c \\exp\\left(-2^{n}\\,\\log\\left(\\frac{c'}{1-c'}\\right)\\right)$$
Lean4
theorem measure_gt_normThreshold_le_exp [IsProbabilityMeasure μ]
(h_rot : (μ.prod μ).map (ContinuousLinearMap.rotation (-(π / 4))) = μ.prod μ) (ha_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a})
(ha_lt : μ {x | ‖x‖ ≤ a} < 1) (n : ℕ) :
μ {x | normThreshold a n < ‖x‖} ≤
μ {x | ‖x‖ ≤ a} * .ofReal (rexp (-Real.log (μ {x | ‖x‖ ≤ a} / (1 - μ {x | ‖x‖ ≤ a})).toReal * 2 ^ n)) :=
by
let c := μ {x | ‖x‖ ≤ a}
have hc_pos : 0 < c := lt_of_lt_of_le (by simp) ha_gt.le
replace hc_lt : c < 1 := ha_lt
have hc_lt_top : c < ∞ := measure_lt_top _ _
have hc_one_sub_lt_top : 1 - c < ∞ := lt_top_of_lt (b := 2) (tsub_le_self.trans_lt (by simp))
have hc_ratio_pos : 0 < (c / (1 - c)).toReal :=
by
rw [ENNReal.toReal_div, div_pos_iff_of_pos_right]
· simp [ENNReal.toReal_pos_iff, hc_pos, hc_lt_top]
· simp [ENNReal.toReal_pos_iff, tsub_pos_iff_lt, hc_lt, hc_one_sub_lt_top]
refine (measure_gt_normThreshold_le_rpow h_rot ha_gt n).trans_eq ?_
congr
rw [← Real.log_inv, mul_comm (Real.log _), ← Real.log_rpow (by positivity), Real.exp_log (by positivity), ←
ENNReal.ofReal_rpow_of_nonneg (by positivity) (by positivity), ENNReal.toReal_div, inv_div, ← ENNReal.toReal_div,
ENNReal.ofReal_toReal]
· norm_cast
· exact ENNReal.div_ne_top (by finiteness) (lt_trans (by simp) ha_gt).ne'
