English
Let a ∈ ℝ. Define a sequence t_n by t_0 = a and t_{n+1} = √2 · t_n + a. Then t_n has closed form t_n = a(1+√2)(√2^{n+1} − 1) for all n ∈ ℕ.
Русский
Пусть a ∈ ℝ. Положим последовательность t_n так, чтобы t_0 = a и t_{n+1} = √2 · t_n + a. Тогда для всех n ∈ ℕ выполняется t_n = a(1+√2)(√2^{n+1} − 1).
LaTeX
$$$\\operatorname{normThreshold}(a,n) = a\\,(1+\\sqrt{2})\\,\\big((\\sqrt{2})^{\\;n+1} - 1\\big)$$$
Lean4
/-- A sequence of real thresholds that will be used to cut the space into annuli.
Chosen such that for a rotation invariant measure, an application of lemma
`measure_le_mul_measure_gt_le_of_map_rotation_eq_self` gives
`μ {x | ‖x‖ ≤ a} * μ {x | normThreshold a (n + 1) < ‖x‖} ≤ μ {x | normThreshold a n < ‖x‖} ^ 2`. -/
noncomputable def normThreshold (a : ℝ) : ℕ → ℝ :=
arithGeom (√2) a a
