English
The function n ↦ ||deriv(z^p(1 + ε(z)))|| grows polynomially with exponent p−1, under the smoothing assumptions, i.e., GrowsPolynomially of the derivative magnitude with exponent p−1.
Русский
Функция n ↦ ||производная от z^p(1 + ε(z))|| растет полиномиально с показателем p−1.
LaTeX
$$GrowsPolynomially (fun n => |d/dz (z^p(1 + ε(z)))|) with exponent (p−1).$$
Lean4
/-- The main proof of the lower-bound part of the Akra-Bazzi theorem. The factor `1 + ε n` does not
change the asymptotic order, but it is needed for the induction step to go through. -/
theorem smoothingFn_mul_asympBound_isBigO_T : (fun (n : ℕ) => (1 + ε n) * asympBound g a b n) =O[atTop] T :=
by
let b' := b (min_bi b) / 2
have hb_pos : 0 < b' := R.bi_min_div_two_pos
rw [isBigO_atTop_iff_eventually_exists_pos]
obtain ⟨c₁, hc₁, h_sumTransform_aux⟩ := R.eventually_atTop_sumTransform_le
filter_upwards [
-- n₀_ge_Rn₀
eventually_ge_atTop R.n₀,
-- h_b_floor
(tendsto_nat_floor_mul_atTop b' hb_pos).eventually_gt_atTop 0,
-- h_smoothing_pos
eventually_forall_ge_atTop.mpr eventually_one_add_smoothingFn_pos,
(tendsto_nat_floor_mul_atTop b' hb_pos).eventually_forall_ge_atTop eventually_one_add_smoothingFn_pos,
-- h_asympBound_pos
eventually_forall_ge_atTop.mpr R.eventually_asympBound_pos,
-- h_asympBound_r_pos
eventually_forall_ge_atTop.mpr R.eventually_asympBound_r_pos,
(tendsto_nat_floor_mul_atTop b' hb_pos).eventually_forall_ge_atTop R.eventually_asympBound_pos,
-- n₀_pos
eventually_gt_atTop 0,
-- h_smoothing_r_pos
eventually_forall_ge_atTop.mpr R.eventually_one_add_smoothingFn_r_pos,
-- bound2
eventually_forall_ge_atTop.mpr R.rpow_p_mul_one_add_smoothingFn_ge,
(tendsto_nat_floor_mul_atTop b' hb_pos).eventually_forall_ge_atTop eventually_one_add_smoothingFn_pos,
-- h_sumTransform
eventually_forall_ge_atTop.mpr h_sumTransform_aux,
-- h_bi_le_r
eventually_forall_ge_atTop.mpr R.eventually_bi_mul_le_r,
-- h_exp
eventually_forall_ge_atTop.mpr (eventually_ge_atTop ⌈exp 1⌉₊)] with n₀ n₀_ge_Rn₀ h_b_floor h_smoothing_pos
h_smoothing_pos' h_asympBound_pos h_asympBound_r_pos h_asympBound_floor n₀_pos h_smoothing_r_pos bound2
h_smoothingFn_floor h_sumTransform h_bi_le_r h_exp
have h_base_nonempty := R.base_nonempty n₀_pos
set base_min : ℝ :=
(Finset.Ico (⌊b' * n₀⌋₊) n₀).inf' h_base_nonempty (fun n => T n / ((1 + ε n) * asympBound g a b n)) with
base_min_def
let C := min (2 * c₁)⁻¹ base_min
have hC_pos : 0 < C := by
refine lt_min (by positivity) ?_
obtain ⟨m, hm_mem, hm⟩ :=
Finset.exists_mem_eq_inf' h_base_nonempty (fun n => T n / ((1 + ε n) * asympBound g a b n))
calc
0 < T m / ((1 + ε m) * asympBound g a b m) :=
by
have H₁ : 0 < T m := R.T_pos _
have H₂ : 0 < 1 + ε m := by
rw [Finset.mem_Ico] at hm_mem
exact h_smoothing_pos' m hm_mem.1
have H₃ : 0 < asympBound g a b m := by
refine R.asympBound_pos m ?_
calc
0 < ⌊b' * n₀⌋₊ := by exact h_b_floor
_ ≤ m := by rw [Finset.mem_Ico] at hm_mem; exact hm_mem.1
positivity
_ = base_min := by rw [base_min_def, hm]
refine
⟨C, hC_pos, fun n hn => ?_⟩
-- Base case: statement is true for `b' * n₀ ≤ n < n₀`
have h_base : ∀ n ∈ Finset.Ico (⌊b' * n₀⌋₊) n₀, C * ((1 + ε n) * asympBound g a b n) ≤ T n :=
by
intro n hn
rw [Finset.mem_Ico] at hn
have htmp1 : 0 < 1 + ε n := h_smoothingFn_floor n hn.1
have htmp2 : 0 < asympBound g a b n := h_asympBound_floor n hn.1
rw [← _root_.le_div_iff₀ (by positivity)]
rw [← Finset.mem_Ico] at hn
calc
T n / ((1 + ε ↑n) * asympBound g a b n) ≥
(Finset.Ico (⌊b' * n₀⌋₊) n₀).inf' h_base_nonempty fun z => T z / ((1 + ε z) * asympBound g a b z) :=
Finset.inf'_le_of_le _ (b := n) hn <| le_refl _
_ ≥ C := min_le_right _ _
have h_asympBound_pos' : 0 < asympBound g a b n := h_asympBound_pos n hn
have h_one_sub_smoothingFn_pos' : 0 < 1 + ε n := h_smoothing_pos n hn
rw [Real.norm_of_nonneg (R.T_nonneg n), Real.norm_of_nonneg (by positivity)]
-- We now prove all other cases by induction
induction n using Nat.strongRecOn with
| ind n
h_ind =>
have b_mul_n₀_le_ri i : ⌊b' * ↑n₀⌋₊ ≤ r i n := by
exact_mod_cast
calc
⌊b' * ↑n₀⌋₊ ≤ b' * n₀ := Nat.floor_le <| by positivity
_ ≤ b' * n := by gcongr
_ ≤ r i n := h_bi_le_r n hn i
have g_pos : 0 ≤ g n := R.g_nonneg n (by positivity)
calc
T n
_ = (∑ i, a i * T (r i n)) + g n := (R.h_rec n <| n₀_ge_Rn₀.trans hn)
_ ≥ (∑ i, a i * (C * ((1 + ε (r i n)) * asympBound g a b (r i n)))) + g n := by
-- Apply the induction hypothesis, or use the base case depending on how large `n` is
gcongr (∑ i, a i * ?_) + g n with i _
· exact le_of_lt <| R.a_pos _
·
cases lt_or_ge (r i n) n₀ with
| inl ri_lt_n₀ => exact h_base _ <| Finset.mem_Ico.mpr ⟨b_mul_n₀_le_ri i, ri_lt_n₀⟩
| inr n₀_le_ri =>
exact
h_ind (r i n) (R.r_lt_n _ _ (n₀_ge_Rn₀.trans hn)) n₀_le_ri (h_asympBound_r_pos _ hn _)
(h_smoothing_r_pos n hn i)
_ =
(∑ i,
a i *
(C * ((1 + ε (r i n)) * ((r i n) ^ (p a b) * (1 + (∑ u ∈ range (r i n), g u / u ^ ((p a b) + 1))))))) +
g n :=
by simp_rw [asympBound_def']
_ =
(∑ i,
C * a i *
((r i n) ^ (p a b) * (1 + ε (r i n)) * ((1 + (∑ u ∈ range (r i n), g u / u ^ ((p a b) + 1)))))) +
g n :=
by congr; ext; ring
_ ≥
(∑ i,
C * a i *
((b i) ^ (p a b) * n ^ (p a b) * (1 + ε n) * ((1 + (∑ u ∈ range (r i n), g u / u ^ ((p a b) + 1)))))) +
g n :=
by
gcongr (∑ i, C * a i * (?_ * ((1 + (∑ u ∈ range (r i n), g u / u ^ ((p a b) + 1)))))) + g n with i
· have := R.a_pos i
positivity
· refine add_nonneg zero_le_one <| Finset.sum_nonneg fun j _ => ?_
rw [div_nonneg_iff]
exact Or.inl ⟨R.g_nonneg j (by positivity), by positivity⟩
· exact bound2 n hn i
_ =
(∑ i,
C * a i *
((b i) ^ (p a b) * n ^ (p a b) * (1 + ε n) *
((1 +
((∑ u ∈ range n, g u / u ^ ((p a b) + 1)) -
(∑ u ∈ Finset.Ico (r i n) n, g u / u ^ ((p a b) + 1))))))) +
g n :=
by
congr; ext i; congr
refine eq_sub_of_add_eq ?_
rw [add_comm]
exact add_eq_of_eq_sub <| Finset.sum_Ico_eq_sub _ <| le_of_lt <| R.r_lt_n i n <| n₀_ge_Rn₀.trans hn
_ =
(∑ i,
C * a i *
((b i) ^ (p a b) * (1 + ε n) *
((n ^ (p a b) * (1 + (∑ u ∈ range n, g u / u ^ ((p a b) + 1))) -
n ^ (p a b) * (∑ u ∈ Finset.Ico (r i n) n, g u / u ^ ((p a b) + 1)))))) +
g n :=
by congr; ext; ring
_ =
(∑ i, C * a i * ((b i) ^ (p a b) * (1 + ε n) * ((asympBound g a b n - sumTransform (p a b) g (r i n) n)))) +
g n :=
by simp_rw [asympBound_def', sumTransform_def]
_ ≥ (∑ i, C * a i * ((b i) ^ (p a b) * (1 + ε n) * ((asympBound g a b n - c₁ * g n)))) + g n :=
by
gcongr with i
· have := R.a_pos i
positivity
· have := R.b_pos i
positivity
· exact h_sumTransform n hn i
_ = (∑ i, C * (1 + ε n) * ((asympBound g a b n - c₁ * g n)) * (a i * (b i) ^ (p a b))) + g n := by congr; ext;
ring
_ = C * (1 + ε n) * (asympBound g a b n - c₁ * g n) + g n := by
rw [← Finset.mul_sum, R.sumCoeffsExp_p_eq_one, mul_one]
_ = C * (1 + ε n) * asympBound g a b n + (1 - C * c₁ * (1 + ε n)) * g n := by ring
_ ≥ C * (1 + ε n) * asympBound g a b n + 0 := by
gcongr
refine mul_nonneg ?_ g_pos
rw [sub_nonneg]
calc
C * c₁ * (1 + ε n)
_ ≤ C * c₁ * 2 := by
gcongr
refine one_add_smoothingFn_le_two ?_
calc
exp 1 ≤ ⌈exp 1⌉₊ := by exact Nat.le_ceil _
_ ≤ n := by exact_mod_cast h_exp n hn
_ = C * (2 * c₁) := by ring
_ ≤ (2 * c₁)⁻¹ * (2 * c₁) := by gcongr; exact min_le_left _ _
_ = c₁⁻¹ * c₁ := by ring
_ = 1 := inv_mul_cancel₀ (by positivity)
_ = C * ((1 + ε n) * asympBound g a b n) := by ring
