real_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two

English

Parallelogram law holds for NNReal norms: ‖x+y‖₊^2 + ‖x−y‖₊^2 = 2(‖x‖₊^2 + ‖y‖₊^2).

Русский

Параллелограммовое тождество верно для nnnorm: ‖x+y‖₊^2 + ‖x−y‖₊^2 = 2(‖x‖₊^2 + ‖y‖₊^2).

LaTeX

$$$\|x+y\|_+^2 + \|x-y\|_+^2 = 2(\|x\|_+^2 + \|y\|_+^2)$$$

Lean4

/-- Polarization identity: The real inner product, in terms of the norm. -/
theorem real_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two (x y : F) :
    ⟪x, y⟫_ℝ = (‖x + y‖ * ‖x + y‖ - ‖x‖ * ‖x‖ - ‖y‖ * ‖y‖) / 2 :=
  re_to_real.symm.trans <| re_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two x y

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