parallelogram_law_with_norm — Mathlib

English

In any inner product space, the norm satisfies the parallelogram identity: ||x+y||^2 + ||x−y||^2 = 2(||x||^2 + ||y||^2).

Русский

В любом пространстве с скалярным произведением норма удовлетворяет параллелограммовому тождеству: ||x+y||^2 + ||x−y||^2 = 2(||x||^2 + ||y||^2).

LaTeX

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

Lean4

theorem parallelogram_law_with_norm (x y : E) : ‖x + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖ = 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) :=
  by
  simp only [← @inner_self_eq_norm_mul_norm 𝕜]
  rw [← re.map_add, parallelogram_law, two_mul, two_mul]
  simp only [re.map_add]

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