abs_cpow_inv_two_im — Mathlib

English

For all x ∈ ℂ, |Im(x^{1/2})| = sqrt((‖x‖ − Re x)/2).

Русский

Для любого x ∈ ℂ, |Im(x^{1/2})| = sqrt((‖x‖ − Re x)/2).

LaTeX

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

Lean4

theorem abs_cpow_inv_two_im (x : ℂ) : |(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, abs_mul,
    abs_of_nonneg (sqrt_nonneg _), abs_sin_half, ← sqrt_mul (norm_nonneg _), ← mul_div_assoc, mul_sub, mul_one,
    norm_mul_cos_arg]

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