English
For complex numbers z and w, under a mild nondegeneracy condition, the norm of z^w equals the real power of |z| to the real part of w divided by exp(arg z times Im w). This gives a closed form for the modulus of complex exponents when defined.
Русский
Для комплексных чисел z и w, при слабо ограниченной невыраженности, модуль z^w равен |z|^{Re(w)} / e^{Re(z) Im(w) ?}, точнее: ||z^w|| = ||z||^{Re w} / exp(arg z · Im w).
LaTeX
$$$\|z^w\| = \|z\|^{\Re w} / e^{\operatorname{Im}(w) \arg(z)}$ (при соответствующих условиях)$$
Lean4
theorem norm_cpow_of_imp {z w : ℂ} (h : z = 0 → w.re = 0 → w = 0) : ‖z ^ w‖ = ‖z‖ ^ w.re / Real.exp (arg z * im w) :=
by
rcases ne_or_eq z 0 with (hz | rfl) <;> [exact norm_cpow_of_ne_zero hz w; rw [norm_zero]]
rcases eq_or_ne w.re 0 with hw | hw
· simp [h rfl hw]
· rw [Real.zero_rpow hw, zero_div, zero_cpow, norm_zero]
exact ne_of_apply_ne re hw
