English
If hl bounds |Im g| and f^g is defined, then f^g = O_l ‖f‖^{Re g}.
Русский
Если гипотеза hl ограничивает |Im g| и f^g определено, то f^g = O_l ‖f‖^{Re g}.
LaTeX
$$$$ (f(\\cdot))^{g(\\cdot)} = O_l \\left( \\|f(\\cdot)\\|^{\\Re(g(\\cdot))} \\right). $$$$
Lean4
theorem isBigO_cpow_rpow (hl : IsBoundedUnder (· ≤ ·) l fun x => |(g x).im|) :
(fun x => f x ^ g x) =O[l] fun x => ‖f x‖ ^ (g x).re :=
calc
(fun x => f x ^ g x) =O[l] (show α → ℝ from fun x => ‖f x‖ ^ (g x).re / Real.exp (arg (f x) * im (g x))) :=
isBigO_of_le _ fun _ => (norm_cpow_le _ _).trans (le_abs_self _)
_ =Θ[l] (show α → ℝ from fun x => ‖f x‖ ^ (g x).re / (1 : ℝ)) :=
((isTheta_refl _ _).div (isTheta_exp_arg_mul_im hl))
_ =ᶠ[l] (show α → ℝ from fun x => ‖f x‖ ^ (g x).re) := by simp only [div_one, EventuallyEq.rfl]
