English
A lower bound inequality: for suitably large n and each i, (r_i(n))^p (1 − ε(r_i(n))) ≤ (b_i n)^p (1 − ε(n)) up to constants, establishing a polynomial growth comparison.
Русский
Нижняя оценка: при достаточно больших n и для каждого i выполняется неравенство (r_i(n))^p(1 − ε(r_i(n))) ≤ (b_i n)^p(1 − ε(n)) до констант, задавая сравнительный полynomial рост.
LaTeX
$$$\\forall i,\\ (r_i(n))^{p}\\,(1 - \\varepsilon(r_i(n))) \\;\\leq\\; C\\,(b_i n)^{p}\\,(1 - \\varepsilon(n)) \\quad \\text{для больших } n.$$$
Lean4
theorem rpow_p_mul_one_sub_smoothingFn_le :
∀ᶠ (n : ℕ) in atTop, ∀ i, (r i n) ^ (p a b) * (1 - ε (r i n)) ≤ (b i) ^ (p a b) * n ^ (p a b) * (1 - ε n) :=
by
rw [Filter.eventually_all]
intro i
let q : ℝ → ℝ := fun x => x ^ (p a b) * (1 - ε x)
have h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1) :=
by
refine
DifferentiableOn.mul (DifferentiableOn.mono (differentiableOn_rpow_const _) fun z hz => ?_)
differentiableOn_one_sub_smoothingFn
rw [Set.mem_compl_singleton_iff]
rw [Set.mem_Ioi] at hz
exact ne_of_gt <| zero_lt_one.trans hz
have h_deriv_q : deriv q =O[atTop] fun x => x ^ ((p a b) - 1) :=
calc
deriv q
_ = deriv fun x => (fun z => z ^ (p a b)) x * (fun z => 1 - ε z) x := by rfl
_ =ᶠ[atTop] fun x => deriv (fun z => z ^ (p a b)) x * (1 - ε x) + x ^ (p a b) * deriv (fun z => 1 - ε z) x :=
by
filter_upwards [eventually_ne_atTop 0, eventually_gt_atTop 1] with x hx hx'
rw [deriv_fun_mul] <;> aesop
_ =O[atTop] fun x => x ^ ((p a b) - 1) :=
by
refine IsBigO.add ?left ?right
case left =>
calc
(fun x => deriv (fun z => z ^ (p a b)) x * (1 - ε x))
_ =O[atTop] fun x => x ^ ((p a b) - 1) * (1 - ε x) :=
(IsBigO.mul (isBigO_deriv_rpow_const_atTop (p a b)) (isBigO_refl _ _))
_ =O[atTop] fun x => x ^ ((p a b) - 1) * 1 :=
(IsBigO.mul (isBigO_refl _ _) isEquivalent_one_sub_smoothingFn_one.isBigO)
_ = fun x => x ^ ((p a b) - 1) := by ext; rw [mul_one]
case right =>
calc
(fun x => x ^ (p a b) * deriv (fun z => 1 - ε z) x)
_ =O[atTop] (fun x => x ^ (p a b) * x⁻¹) :=
(IsBigO.mul (isBigO_refl _ _) isLittleO_deriv_one_sub_smoothingFn.isBigO)
_ =ᶠ[atTop] fun x => x ^ ((p a b) - 1) :=
by
filter_upwards [eventually_gt_atTop 0] with x hx
rw [← Real.rpow_neg_one, ← Real.rpow_add hx, ← sub_eq_add_neg]
have h_main_norm :
(fun (n : ℕ) => ‖q (r i n) - q (b i * n)‖) ≤ᶠ[atTop] fun (n : ℕ) =>
‖(b i) ^ (p a b) * n ^ (p a b) * (ε (b i * n) - ε n)‖ :=
by
refine IsLittleO.eventuallyLE ?_
calc
(fun (n : ℕ) => q (r i n) - q (b i * n))
_ =O[atTop] fun n => (deriv q n) * (r i n - b i * n) :=
(R.isBigO_apply_r_sub_b q h_diff_q (growsPolynomially_deriv_rpow_p_mul_one_sub_smoothingFn (p a b)) i)
_ =o[atTop] fun n => (deriv q n) * (n / log n ^ 2) := (IsBigO.mul_isLittleO (isBigO_refl _ _) (R.dist_r_b i))
_ =O[atTop] fun n => n ^ ((p a b) - 1) * (n / log n ^ 2) :=
(IsBigO.mul (IsBigO.natCast_atTop h_deriv_q) (isBigO_refl _ _))
_ =ᶠ[atTop] fun n => n ^ (p a b) / (log n) ^ 2 :=
by
filter_upwards [eventually_ne_atTop 0] with n hn
have hn' : (n : ℝ) ≠ 0 := by positivity
simp [← mul_div_assoc, ← Real.rpow_add_one hn']
_ = fun (n : ℕ) => (n : ℝ) ^ (p a b) * (1 / (log n) ^ 2) := by simp_rw [mul_div, mul_one]
_ =Θ[atTop] fun (n : ℕ) => (b i) ^ (p a b) * n ^ (p a b) * (1 / (log n) ^ 2) :=
by
refine IsTheta.symm ?_
simp_rw [mul_assoc]
refine IsTheta.const_mul_left ?_ (isTheta_refl _ _)
have := R.b_pos i; positivity
_ =Θ[atTop] fun (n : ℕ) => (b i) ^ (p a b) * n ^ (p a b) * (ε (b i * n) - ε n) :=
IsTheta.symm <| IsTheta.mul (isTheta_refl _ _) <| R.isTheta_smoothingFn_sub_self i
have h_main :
(fun (n : ℕ) => q (r i n) - q (b i * n)) ≤ᶠ[atTop] fun (n : ℕ) =>
(b i) ^ (p a b) * n ^ (p a b) * (ε (b i * n) - ε n) :=
by
calc
(fun (n : ℕ) => q (r i n) - q (b i * n))
_ ≤ᶠ[atTop] fun (n : ℕ) => ‖q (r i n) - q (b i * n)‖ := by filter_upwards with _ using le_norm_self _
_ ≤ᶠ[atTop] fun (n : ℕ) => ‖(b i) ^ (p a b) * n ^ (p a b) * (ε (b i * n) - ε n)‖ := h_main_norm
_ =ᶠ[atTop] fun (n : ℕ) => (b i) ^ (p a b) * n ^ (p a b) * (ε (b i * n) - ε n) :=
by
filter_upwards [eventually_gt_atTop ⌈(b i)⁻¹⌉₊, eventually_gt_atTop 1] with n hn hn'
refine norm_of_nonneg ?_
have h₁ := R.b_pos i
have h₂ : 0 ≤ ε (b i * n) - ε n :=
by
refine sub_nonneg_of_le <| (strictAntiOn_smoothingFn.le_iff_ge ?n_gt_one ?bn_gt_one).mpr ?le
case n_gt_one => rwa [Set.mem_Ioi, Nat.one_lt_cast]
case bn_gt_one =>
calc
1 = b i * (b i)⁻¹ := by rw [mul_inv_cancel₀ (by positivity)]
_ ≤ b i * ⌈(b i)⁻¹⌉₊ := by gcongr; exact Nat.le_ceil _
_ < b i * n := by gcongr
case le =>
calc
b i * n
_ ≤ 1 * n := by have := R.b_lt_one i; gcongr
_ = n := by rw [one_mul]
positivity
filter_upwards [h_main] with n hn
have h₁ :
q (b i * n) + (b i) ^ (p a b) * n ^ (p a b) * (ε (b i * n) - ε n) = (b i) ^ (p a b) * n ^ (p a b) * (1 - ε n) :=
by
have := R.b_pos i
simp only [q, mul_rpow (by positivity : (0 : ℝ) ≤ b i) (by positivity : (0 : ℝ) ≤ n)]
ring
change q (r i n) ≤ (b i) ^ (p a b) * n ^ (p a b) * (1 - ε n)
rw [← h₁, ← sub_le_iff_le_add']
exact hn
