English
For the AkraBazziRecurrence R, the smoothing differences satisfy the asymptotic equivalence described earlier for each i.
Русский
Для фактора R акрави базиса сглаживание обладает описанным ранее асимптотическим эквивалентным поведением для каждого i.
LaTeX
$$$$\forall i:\; (ε(b_i n) - ε(n)) \sim -\frac{\log(b_i)}{(\log n)^2}.$$$$
Lean4
theorem isEquivalent_smoothingFn_sub_self (i : α) :
(fun (n : ℕ) => ε (b i * n) - ε n) ~[atTop] fun n => -log (b i) / (log n) ^ 2 := by
calc
(fun (n : ℕ) => 1 / log (b i * n) - 1 / log n)
_ =ᶠ[atTop] fun (n : ℕ) => (log n - log (b i * n)) / (log (b i * n) * log n) :=
by
filter_upwards [eventually_gt_atTop 1, R.eventually_log_b_mul_pos] with n hn hn'
have h_log_pos : 0 < log n := Real.log_pos <| by simp_all
simp only [one_div]
rw [inv_sub_inv (by have := hn' i; positivity) (by aesop)]
_ =ᶠ[atTop] (fun (n : ℕ) ↦ (log n - log (b i) - log n) / ((log (b i) + log n) * log n)) :=
by
filter_upwards [eventually_ne_atTop 0] with n hn
have : 0 < b i := R.b_pos i
rw [log_mul (by positivity) (by simp_all), sub_add_eq_sub_sub]
_ = (fun (n : ℕ) => -log (b i) / ((log (b i) + log n) * log n)) := by ext; congr; ring
_ ~[atTop] (fun (n : ℕ) => -log (b i) / (log n * log n)) :=
by
refine IsEquivalent.div (IsEquivalent.refl) <| IsEquivalent.mul ?_ (IsEquivalent.refl)
have : (fun (n : ℕ) => log (b i) + log n) = fun (n : ℕ) => log n + log (b i) := by ext; simp [add_comm]
rw [this]
exact
IsEquivalent.add_isLittleO IsEquivalent.refl <|
IsLittleO.natCast_atTop (f := fun (_ : ℝ) => log (b i)) isLittleO_const_log_atTop
_ = (fun (n : ℕ) => -log (b i) / (log n) ^ 2) := by ext; congr 1; rw [← pow_two]
