English
If b1 < b2, then z^a1 e^{b1 z} = o_l z^a2 e^{b2 z}.
Русский
Если b1 < b2, то z^a1 e^{b1 z} = o_l z^a2 e^{b2 z}.
LaTeX
$$$\\forall {b_1 b_2 : \\mathbb{R}},\\; (\\operatorname{hb}: b_1 < b_2) \\to \\forall a_1 a_2:\\mathbb{C},\\; (z \\mapsto z^{a_1} e^{b_1 z}) =o_l (z \\mapsto z^{a_2} e^{b_2 z})$$$
Lean4
/-- If `l : Filter ℂ` is an "exponential comparison filter", then for any complex `a₁`, `a₂` and any
real `b₁ < b₂`, we have `(fun z ↦ z ^ a₁ * exp (b₁ * z)) =o[l] (fun z ↦ z ^ a₂ * exp (b₂ * z))`. -/
theorem isLittleO_cpow_mul_exp {b₁ b₂ : ℝ} (hl : IsExpCmpFilter l) (hb : b₁ < b₂) (a₁ a₂ : ℂ) :
(fun z => z ^ a₁ * exp (b₁ * z)) =o[l] fun z => z ^ a₂ * exp (b₂ * z) :=
calc
(fun z => z ^ a₁ * exp (b₁ * z)) =ᶠ[l] fun z => z ^ a₂ * exp (b₁ * z) * z ^ (a₁ - a₂) :=
hl.eventually_ne.mono fun z hz => by
simp only
rw [mul_right_comm, ← cpow_add _ _ hz, add_sub_cancel]
_ =o[l] fun z => z ^ a₂ * exp (b₁ * z) * exp (↑(b₂ - b₁) * z) :=
((isBigO_refl (fun z => z ^ a₂ * exp (b₁ * z)) l).mul_isLittleO <| hl.isLittleO_cpow_exp _ (sub_pos.2 hb))
_ =ᶠ[l] fun z => z ^ a₂ * exp (b₂ * z) :=
by
simp only [ofReal_sub, sub_mul, mul_assoc, ← exp_add, add_sub_cancel]
norm_cast
