cpow_inv_two_im_eq_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_sqrt {x : ℂ} (hx : 0 ≤ x.im) : (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_sqrt,
    ← sqrt_mul (norm_nonneg _), ← mul_div_assoc, mul_sub, mul_one, norm_mul_cos_arg]
  · rwa [arg_nonneg_iff]
  · linarith [pi_pos, arg_le_pi x]

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