re_inner_eq_norm_add_mul_self_sub_norm_sub_mul_self_div_four

English

The inner product is determined by the norms of x±y and x±iy: ⟪x,y⟫ = 1/4[(||x+y||^2−||x−y||^2) + i(||x−iy||^2−||x+iy||^2)].

Русский

Скалярное произведение определяется через квадраты норм x±y и x±iy: ⟪x,y⟫ = 1/4[(||x+y||^2−||x−y||^2) + i(||x−iy||^2−||x+iy||^2)].

LaTeX

$$$\langle x,y\rangle = \dfrac{(\|x+y\|^2 - \|x-y\|^2) + i(\|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_add_mul_self_sub_norm_sub_mul_self_div_four (x y : E) :
    re ⟪x, y⟫ = (‖x + y‖ * ‖x + y‖ - ‖x - y‖ * ‖x - y‖) / 4 :=
  by
  rw [@norm_add_mul_self 𝕜, @norm_sub_mul_self 𝕜]
  ring

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