norm_cpow_eq_rpow_re_of_pos — Mathlib

English

If x > 0 is real and y is complex, then ∥(x)^y∥ = x^{Re y}.

Русский

Если x > 0 реально и y комплексно, тогда ∥x^y∥ = x^{Re y}.

LaTeX

$$$x>0 \Rightarrow \|x^{y}\| = x^{\Re y}$$$

Lean4

theorem norm_cpow_eq_rpow_re_of_pos {x : ℝ} (hx : 0 < x) (y : ℂ) : ‖(x : ℂ) ^ y‖ = x ^ y.re := by
  rw [norm_cpow_of_ne_zero (ofReal_ne_zero.mpr hx.ne'), arg_ofReal_of_nonneg hx.le, zero_mul, Real.exp_zero, div_one,
    Complex.norm_of_nonneg hx.le]

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