English
For hp ≠ 0, the derivative of z^p(1 + ε(z)) has the same asymptotic order as z^{p−1}: deriv(z^p(1 + ε(z))) ~ p z^{p−1}.
Русский
При hp ≠ 0 производная z^p(1 + ε(z)) имеет порядок роста, равный z^{p−1}: d/dz(z^p(1 + ε(z))) ~ p z^{p−1}.
LaTeX
$$$\\displaystyle \\frac{d}{dz}\\bigl(z^p(1 + \\varepsilon(z))\\bigr) \\sim p\\,z^{p-1} \\quad (z \\to \\infty).$$$
Lean4
theorem isBigO_apply_r_sub_b (q : ℝ → ℝ) (hq_diff : DifferentiableOn ℝ q (Set.Ioi 1))
(hq_poly : GrowsPolynomially fun x => ‖deriv q x‖) (i : α) :
(fun n => q (r i n) - q (b i * n)) =O[atTop] fun n => (deriv q n) * (r i n - b i * n) :=
by
let b' := b (min_bi b) / 2
have hb_pos : 0 < b' := by have := R.b_pos (min_bi b); positivity
have hb_lt_one : b' < 1 :=
calc
b (min_bi b) / 2
_ < b (min_bi b) := (div_two_lt_of_pos (R.b_pos (min_bi b)))
_ < 1 := R.b_lt_one (min_bi b)
have hb : b' ∈ Set.Ioo 0 1 := ⟨hb_pos, hb_lt_one⟩
have hb' (i) : b' ≤ b i :=
calc
b (min_bi b) / 2
_ ≤ b i / 2 := by gcongr; aesop
_ ≤ b i := le_of_lt <| div_two_lt_of_pos (R.b_pos i)
obtain ⟨c₁, _, c₂, _, hq_poly⟩ := hq_poly b' hb
rw [isBigO_iff]
refine ⟨c₂, ?_⟩
have h_tendsto : Tendsto (fun x => b' * x) atTop atTop := Tendsto.const_mul_atTop hb_pos tendsto_id
filter_upwards [hq_poly.natCast_atTop, R.eventually_bi_mul_le_r, eventually_ge_atTop R.n₀, eventually_gt_atTop 0,
(h_tendsto.eventually_gt_atTop 1).natCast_atTop] with n hn h_bi_le_r h_ge_n₀ h_n_pos h_bn
rw [norm_mul, ← mul_assoc]
refine
Convex.norm_image_sub_le_of_norm_deriv_le (s := Set.Icc (b' * n) n) (fun z hz => ?diff) (fun z hz => (hn z hz).2)
(convex_Icc _ _) ?mem_Icc <|
⟨h_bi_le_r i, by exact_mod_cast (le_of_lt (R.r_lt_n i n h_ge_n₀))⟩
case diff =>
refine hq_diff.differentiableAt (Ioi_mem_nhds ?_)
calc
1 < b' * n := h_bn
_ ≤ z := hz.1
case mem_Icc =>
refine ⟨by gcongr; exact hb' i, ?_⟩
calc
b i * n ≤ 1 * n := by gcongr; exact le_of_lt <| R.b_lt_one i
_ = n := by simp
