cpow_ofReal — Mathlib

English

For a complex x and real y, x^y has the polar form with modulus |x|^y and angle y·arg x.

Русский

Для комплексного числа x и вещественного y степенная функция имеет полярную форму с модулем |x|^y и углом y·arg x.

LaTeX

$$$x^y = |x|^y (\cos(y\arg x) + i \sin(y\arg x))$$$

Lean4

theorem cpow_ofReal (x : ℂ) (y : ℝ) : x ^ (y : ℂ) = ↑(‖x‖ ^ y) * (Real.cos (arg x * y) + Real.sin (arg x * y) * I) :=
  by
  rcases eq_or_ne x 0 with rfl | hx
  · simp [ofReal_cpow le_rfl]
  · rw [cpow_def_of_ne_zero hx, exp_eq_exp_re_mul_sin_add_cos, mul_comm (log x)]
    norm_cast
    rw [re_ofReal_mul, im_ofReal_mul, log_re, log_im, mul_comm y, mul_comm y, Real.exp_mul, Real.exp_log]
    rwa [norm_pos_iff]

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