English
For any complex a and any b>0, z^a = o_l exp(b z) along l.
Русский
Для любого комплексного a и b>0, z^a = o_l exp(b z) вдоль l.
LaTeX
$$$\\forall a:\\,\\mathbb{C},\\; \\forall b>0:\\; (z \\mapsto z^a) =o_l (z \\mapsto \\exp(b z))$$$
Lean4
/-- If `l : Filter ℂ` is an "exponential comparison filter", then for any complex `a` and any
positive real `b`, we have `(fun z ↦ z ^ a) =o[l] (fun z ↦ exp (b * z))`. -/
theorem isLittleO_cpow_exp (hl : IsExpCmpFilter l) (a : ℂ) {b : ℝ} (hb : 0 < b) :
(fun z => z ^ a) =o[l] fun z => exp (b * z) :=
calc
(fun z => z ^ a) =Θ[l] fun z => Real.exp (re a * Real.log ‖z‖) := hl.isTheta_cpow_exp_re_mul_log a
_ =o[l] fun z => exp (b * z) :=
IsLittleO.of_norm_right <|
by
simp only [norm_exp, re_ofReal_mul, Real.isLittleO_exp_comp_exp_comp]
refine (IsEquivalent.refl.sub_isLittleO ?_).symm.tendsto_atTop (hl.tendsto_re.const_mul_atTop hb)
exact (hl.isLittleO_log_norm_re.const_mul_left _).const_mul_right hb.ne'
