re_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two

English

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

Русский

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

LaTeX

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

Lean4

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

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