English
The inner product is given by norms of x±y and x±iy via a 1/4 combination; equivalently, ⟪x,y⟫ = 1/4[(‖x+y‖^2−‖x−y‖^2) + i(‖x−iy‖^2−‖x+iy‖^2)].
Русский
Скалярное произведение задается через нормы x±y и x±iy через линейную комбинацию 1/4.
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 inner product, in terms of the norm. -/
theorem inner_eq_sum_norm_sq_div_four (x y : E) :
⟪x, y⟫ = ((‖x + y‖ : 𝕜) ^ 2 - (‖x - y‖ : 𝕜) ^ 2 + ((‖x - IK • y‖ : 𝕜) ^ 2 - (‖x + IK • y‖ : 𝕜) ^ 2) * IK) / 4 :=
by
rw [← re_add_im ⟪x, y⟫, re_inner_eq_norm_add_mul_self_sub_norm_sub_mul_self_div_four,
im_inner_eq_norm_sub_i_smul_mul_self_sub_norm_add_i_smul_mul_self_div_four]
push_cast
simp only [sq, ← mul_div_right_comm, ← add_div]
