norm_ofReal_cpow_eventually_eq_atTop

English

For complex z,w with mild nondegeneracy, ∥z^w∥ = ∥z∥^{Re w} / exp( Arg(z) · Im w).

Русский

Для комплексных z,w при некоторых предположениях, ∥z^w∥ = ∥z∥^{Re w} / exp( Arg(z) · Im w ).

LaTeX

$$$\text{If mild conditions hold: } \|z^{w}\| = \|z\|^{\Re w} / e^{\operatorname{Arg}(z) \cdot \Im w}$$$

Lean4

theorem norm_ofReal_cpow_eventually_eq_atTop (c : ℂ) : (fun t : ℝ ↦ ‖(t : ℂ) ^ c‖) =ᶠ[atTop] fun t ↦ t ^ c.re :=
  by
  filter_upwards [eventually_gt_atTop 0] with t ht
  rw [norm_cpow_eq_rpow_re_of_pos ht]

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