English
There exists an inner product on E extending the given norm (Fréchet–von Neumann–Jordan).
Русский
Существует внутреноe произведение на E, согласующееся с данной нормой (теорема Фреше–фон Неймана–Жордана).
LaTeX
$$$\exists \langle\cdot,\cdot\rangle\ on\ E\ s.t.\, \|x\|^{2} = \langle x,x\rangle$$$
Lean4
/-- **Fréchet–von Neumann–Jordan Theorem**. A normed space `E` whose norm satisfies the
parallelogram identity can be given a compatible inner product. -/
noncomputable def ofNorm (h : ∀ x y : E, ‖x + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖ = 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) :
InnerProductSpace 𝕜 E :=
haveI : InnerProductSpaceable E := ⟨h⟩
{ inner := inner_ 𝕜
norm_sq_eq_re_inner := inner_.norm_sq
conj_inner_symm := inner_.conj_symm
add_left := InnerProductSpaceable.add_left
smul_left := fun _ _ _ => innerProp _ _ _ }
