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]