English
Let μ be a measure on a normed space whose product is invariant under rotation, with a ∈ ℝ and n ∈ ℕ. Then μ({x : ‖x‖ ≤ a}) · μ({x : ‖x‖ > normThreshold(a,n+1)}) ≤ μ({x : ‖x‖ > normThreshold(a,n)})^2.
Русский
Пусть μ — мера на нормированном пространстве, чья пара μ×μ сохраняется при вращении; для фиксированных a ∈ ℝ и n ∈ ℕ выполняется: μ({x : ‖x‖ ≤ a}) · μ({x : ‖x‖ > normThreshold(a,n+1)}) ≤ μ({x : ‖x‖ > normThreshold(a,n)})^2.
LaTeX
$$$\\mu\\{x : \\|x\\| \\le a\\} \\;\\cdot\\; \\mu\\{x : \\|x\\| > \\operatorname{normThreshold}(a,n+1)\\} \\le \\mu\\{x : \\|x\\| > \\operatorname{normThreshold}(a,n)\\}^2$$$
Lean4
theorem measure_le_mul_measure_gt_normThreshold_le_of_map_rotation_eq_self [SFinite μ]
(h_rot : (μ.prod μ).map (ContinuousLinearMap.rotation (-(π / 4))) = μ.prod μ) (a : ℝ) (n : ℕ) :
μ {x | ‖x‖ ≤ a} * μ {x | normThreshold a (n + 1) < ‖x‖} ≤ μ {x | normThreshold a n < ‖x‖} ^ 2 :=
by
convert measure_le_mul_measure_gt_le_of_map_rotation_eq_self h_rot _ _
simp [normThreshold_add_one]
