re_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two

English

The imaginary part of the inner product is determined by norms via polarization: Im⟪x,y⟫ = (||x−iy||^2 − ||x+iy||^2)/(4).

Русский

Мнимая часть скалярного произведения задается через нормы: Im⟪x,y⟫ = (||x−iy||^2 − ||x+iy||^2)/4.

LaTeX

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

Lean4

/-- Polarization identity: The real part of the inner product, in terms of the norm. -/
theorem re_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two (x y : E) :
    re ⟪x, y⟫ = (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x - y‖ * ‖x - y‖) / 2 :=
  by
  rw [@norm_sub_mul_self 𝕜]
  ring

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