English
Let c = μ({‖x‖ ≤ a}). If μ({‖x‖ ≤ a}) > 1/2, then for all n, μ({normThreshold(a,n) < ‖x‖}) ≤ c · ((1−c)/c)^{2^n}. (This uses rotation-invariant μ.)
Русский
Пусть c = μ({‖x‖ ≤ a}). Если μ({‖x‖ ≤ a}) > 1/2, то для всех n имеем μ({normThreshold(a,n) < ‖x‖}) ≤ c · ((1−c)/c)^{2^n}.
LaTeX
$$$c := \\mu\\{x : \\|x\\| \\le a\\},\\quad c>\\tfrac12:\\quad \\mu\\{x : \\|x\\| > \\operatorname{normThreshold}(a,n)\\} \\le c\\left(\\frac{1-c}{c}\\right)^{2^n}$$
Lean4
theorem measure_gt_normThreshold_le_rpow [IsProbabilityMeasure μ]
(h_rot : (μ.prod μ).map (ContinuousLinearMap.rotation (-(π / 4))) = μ.prod μ) (ha_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a})
(n : ℕ) : μ {x | normThreshold a n < ‖x‖} ≤ μ {x | ‖x‖ ≤ a} * ((1 - μ {x | ‖x‖ ≤ a}) / μ {x | ‖x‖ ≤ a}) ^ (2 ^ n) :=
by
let c := μ {x | ‖x‖ ≤ a}
replace hc_gt : 2⁻¹ < c := ha_gt
have hc_pos : 0 < c := lt_of_lt_of_le (by simp) hc_gt.le
have hc_lt_top : c < ∞ := measure_lt_top _ _
induction n with
| zero =>
simp only [pow_zero, pow_one, normThreshold_zero]
rw [ENNReal.mul_div_cancel hc_pos.ne' hc_lt_top.ne]
refine le_of_eq ?_
rw [← prob_compl_eq_one_sub (measurableSet_le (by fun_prop) (by fun_prop))]
congr with x
simp
| succ n
hn =>
have h_mul_le : c * μ {x | normThreshold a (n + 1) < ‖x‖} ≤ μ {x | normThreshold a n < ‖x‖} ^ 2 :=
measure_le_mul_measure_gt_normThreshold_le_of_map_rotation_eq_self h_rot _ _
calc
μ {x | normThreshold a (n + 1) < ‖x‖}
_ = c⁻¹ * (c * μ {x | normThreshold a (n + 1) < ‖x‖}) := by
rw [← mul_assoc, ENNReal.inv_mul_cancel hc_pos.ne' hc_lt_top.ne, one_mul]
_ ≤ c⁻¹ * μ {x | normThreshold a n < ‖x‖} ^ 2 := by gcongr
_ ≤ c⁻¹ * (c * ((1 - c) / c) ^ 2 ^ n) ^ 2 := by gcongr
_ = c * ((1 - c) / c) ^ 2 ^ (n + 1) :=
by
rw [mul_pow, ← pow_mul, ← mul_assoc, pow_two, ← mul_assoc, ENNReal.inv_mul_cancel hc_pos.ne' hc_lt_top.ne,
one_mul]
congr
