cpow_inv_two_im_eq_neg_sqrt — Mathlib

English

For x ∈ ℂ with x.im < 0, Im(x^{1/2}) = - sqrt((‖x‖ − Re x)/2).

Русский

Для x ∈ ℂ при x.im < 0, Im(x^{1/2}) = - sqrt((‖x‖ − Re x)/2).

LaTeX

$$For x ∈ ℂ, Im( x^{1/2} ) = -\sqrt{ ( \|x\| - Re(x) ) / 2 }$$

Lean4

theorem cpow_inv_two_im_eq_neg_sqrt {x : ℂ} (hx : x.im < 0) : (x ^ (2⁻¹ : ℂ)).im = -√((‖x‖ - x.re) / 2) :=
  by
  rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_im, ← div_eq_mul_inv, ← one_div, ← Real.sqrt_eq_rpow,
    sin_half_eq_neg_sqrt, mul_neg, ← sqrt_mul (norm_nonneg _), ← mul_div_assoc, mul_sub, mul_one, norm_mul_cos_arg]
  · linarith [pi_pos, neg_pi_lt_arg x]
  · exact (arg_neg_iff.2 hx).le

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