isTheta_cpow_exp_re_mul_log — Mathlib

English

The power function z^a is Theta of ||z||^{Re a} and equals exp(Re a · log ||z||) asymptotically.

Русский

Функция z^a является Theta(||z||^{Re a}) и асимптотически равна exp(Re a · log ||z||).

LaTeX

$$$\\forall l:\\,\\mathsf{IsExpCmpFilter}\\ l \\to \\Big( (z \\mapsto z^a) =_\\Theta_l (\\lVert z\\rVert)^{\\operatorname{Re} a} \\Big) \\\\to (z \\mapsto \\lVert z\\rVert)^{\\operatorname{Re} a} =_\\text{a.e.}_l (\\exp (\\operatorname{Re} a \\cdot \\log \\lVert z\\rVert))$$$

Lean4

theorem isTheta_cpow_exp_re_mul_log (hl : IsExpCmpFilter l) (a : ℂ) :
    (· ^ a) =Θ[l] fun z ↦ Real.exp (re a * Real.log ‖z‖) :=
  calc
    (fun z => z ^ a) =Θ[l] (fun z : ℂ => ‖z‖ ^ re a) := isTheta_cpow_const_rpow fun _ _ => hl.eventually_ne
    _ =ᶠ[l] fun z => Real.exp (re a * Real.log ‖z‖) :=
      (hl.eventually_ne.mono fun z hz => by simp [Real.rpow_def_of_pos, norm_pos_iff.mpr hz, mul_comm])

Похожие утверждения