English
If x < 0 and y ∈ ℝ, then x^y = exp(y log x) cos(π y).
Русский
Пусть x < 0 и y ∈ ℝ. Тогда x^y = e^{y log x} cos(π y).
LaTeX
$$$\\forall x,y \\in \\mathbb{R}, x < 0 \\Rightarrow x^y = e^{(\\log x) \\cdot y} \\cos(\\pi y)$$$
Lean4
theorem rpow_def_of_neg {x : ℝ} (hx : x < 0) (y : ℝ) : x ^ y = exp (log x * y) * cos (y * π) :=
by
rw [rpow_def, Complex.cpow_def, if_neg]
· have : Complex.log x * y = ↑(log (-x) * y) + ↑(y * π) * Complex.I :=
by
simp only [Complex.log, Complex.norm_real, norm_eq_abs, abs_of_neg hx, log_neg_eq_log,
Complex.arg_ofReal_of_neg hx, Complex.ofReal_mul]
ring
rw [this, Complex.exp_add_mul_I, ← Complex.ofReal_exp, ← Complex.ofReal_cos, ← Complex.ofReal_sin, mul_add, ←
Complex.ofReal_mul, ← mul_assoc, ← Complex.ofReal_mul, Complex.add_re, Complex.ofReal_re, Complex.mul_re,
Complex.I_re, Complex.ofReal_im, Real.log_neg_eq_log]
ring
· rw [Complex.ofReal_eq_zero]
exact ne_of_lt hx
