isTheta_cpow_const_rpow — Mathlib

English

If the real part of b is zero and b ≠ 0, and f ≠ 0 eventually, then f^b = Θ_l ‖f‖^{b.re}.

Русский

Если Re(b) = 0 и b ≠ 0 и f ≠ 0 почти везде, тогда f^b = Θ_l ‖f‖^{Re(b)}.

LaTeX

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

Lean4

theorem isTheta_cpow_const_rpow {b : ℂ} (hl : b.re = 0 → b ≠ 0 → ∀ᶠ x in l, f x ≠ 0) :
    (fun x => f x ^ b) =Θ[l] fun x => ‖f x‖ ^ b.re :=
  isTheta_cpow_rpow isBoundedUnder_const <| by
    simpa only [eventually_imp_distrib_right, not_imp_not, Imp.swap (a := b.re = 0)] using hl

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