im_inner_eq_norm_sub_i_smul_mul_self_sub_norm_add_i_smul_mul_self_div_four

English

Another form of the imaginary-part polarization expresses Im⟪x,y⟫ via norms of x±I y.

Русский

Еще одно выражение мнимой части через нормы x±I y.

LaTeX

$$$\operatorname{Im}\langle x,y\rangle = \dfrac{\|x- \mathbf{i}y\|^2 - \|x+ \mathbf{i}y\|^2}{4}$$$

Lean4

/-- Polarization identity: The imaginary part of the inner product, in terms of the norm. -/
theorem im_inner_eq_norm_sub_i_smul_mul_self_sub_norm_add_i_smul_mul_self_div_four (x y : E) :
    im ⟪x, y⟫ = (‖x - IK • y‖ * ‖x - IK • y‖ - ‖x + IK • y‖ * ‖x + IK • y‖) / 4 :=
  by
  simp only [@norm_add_mul_self 𝕜, @norm_sub_mul_self 𝕜, inner_smul_right, I_mul_re]
  ring

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