Theorems · Definition · functional analysis

InnerProductSpace.ofNorm

(𝕜 : Type u_1) →
  [inst : RCLike 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [NormedSpace 𝕜 E] →
          (∀ (x y : E), ‖x + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖ = 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) → InnerProductSpace 𝕜 E

Fréchet–von Neumann–Jordan Theorem. A normed space E whose norm satisfies the parallelogram identity can be given a compatible inner product.

Defined in

Mathlib.Analysis.InnerProductSpace.OfNorm

Cited by

0 results in Mathlib

Foundations

Depth 174 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeNormedAddCommGroupNormedSpace