isTheta_cpow_rpow — Mathlib

English

If hl and hl_im hold, then f^g is Θ_l (‖f‖^{Re g}).

Русский

При выполнении условий hl и hl_im имеем f^g = Θ_l(‖f‖^{Re g}).

LaTeX

$$$$ (f(\\cdot))^{g(\\cdot)} = Θ_l \\left( \\|f(\\cdot)\\|^{\\Re(g(\\cdot))} \\right). $$$$

Lean4

theorem isTheta_cpow_rpow (hl_im : IsBoundedUnder (· ≤ ·) l fun x => |(g x).im|)
    (hl : ∀ᶠ x in l, f x = 0 → re (g x) = 0 → g x = 0) : (fun x => f x ^ g x) =Θ[l] fun x => ‖f x‖ ^ (g x).re :=
  calc
    (fun x => f x ^ g x) =Θ[l] (fun x => ‖f x‖ ^ (g x).re / Real.exp (arg (f x) * im (g x))) :=
      .of_norm_eventuallyEq <| hl.mono fun _ => norm_cpow_of_imp
    _ =Θ[l] fun x => ‖f x‖ ^ (g x).re / (1 : ℝ) := ((isTheta_refl _ _).div (isTheta_exp_arg_mul_im hl_im))
    _ =ᶠ[l] (fun x => ‖f x‖ ^ (g x).re) := by simp only [div_one, EventuallyEq.rfl]

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