# Inner product space derived from a norm #

This file defines an InnerProductSpace instance from a norm that respects the parallellogram identity. The parallelogram identity is a way to express the inner product of x and y in terms of the norms of x, y, x + y, x - y.

## Main results #

• InnerProductSpace.ofNorm: a normed space whose norm respects the parallellogram identity, can be seen as an inner product space.

## Implementation notes #

We define inner_

$$\langle x, y \rangle := \frac{1}{4} (‖x + y‖^2 - ‖x - y‖^2 + i ‖ix + y‖ ^ 2 - i ‖ix - y‖^2)$$

and use the parallelogram identity

$$‖x + y‖^2 + ‖x - y‖^2 = 2 (‖x‖^2 + ‖y‖^2)$$

to prove it is an inner product, i.e., that it is conjugate-symmetric (inner_.conj_symm) and linear in the first argument. add_left is proved by judicious application of the parallelogram identity followed by tedious arithmetic. smul_left is proved step by step, first noting that $\langle λ x, y \rangle = λ \langle x, y \rangle$ for $λ ∈ ℕ$, $λ = -1$, hence $λ ∈ ℤ$ and $λ ∈ ℚ$ by arithmetic. Then by continuity and the fact that ℚ is dense in ℝ, the same is true for ℝ. The case of ℂ then follows by applying the result for ℝ and more arithmetic.

## TODO #

Move upstream to Analysis.InnerProductSpace.Basic.

## References #

• [Jordan, P. and von Neumann, J., On inner products in linear, metric spaces][Jordan1935]
• https://math.stackexchange.com/questions/21792/norms-induced-by-inner-products-and-the-parallelogram-law
• https://math.dartmouth.edu/archive/m113w10/public_html/jordan-vneumann-thm.pdf

## Tags #

inner product space, Hilbert space, norm

Predicate for the parallelogram identity to hold in a normed group. This is a scalar-less version of InnerProductSpace. If you have an InnerProductSpaceable assumption, you can locally upgrade that to InnerProductSpace 𝕜 E using casesI nonempty_innerProductSpace 𝕜 E.

Instances
theorem InnerProductSpace.toInnerProductSpaceable (𝕜 : Type u_1) [] {E : Type u_2} [] :
Equations
• =
theorem InnerProductSpaceable.innerProp_neg_one {𝕜 : Type u_1} [] {E : Type u_2} [] :
theorem Continuous.inner_ {𝕜 : Type u_1} [] {E : Type u_2} [] {f : E} {g : E} (hf : ) (hg : ) :
Continuous fun (x : ) => inner_ 𝕜 (f x) (g x)
theorem InnerProductSpaceable.inner_.norm_sq {𝕜 : Type u_1} [] {E : Type u_2} [] (x : E) :
x ^ 2 = RCLike.re (inner_ 𝕜 x x)
theorem InnerProductSpaceable.inner_.conj_symm {𝕜 : Type u_1} [] {E : Type u_2} [] (x : E) (y : E) :
() (inner_ 𝕜 y x) = inner_ 𝕜 x y
theorem InnerProductSpaceable.add_left {𝕜 : Type u_1} [] {E : Type u_2} [] (x : E) (y : E) (z : E) :
inner_ 𝕜 (x + y) z = inner_ 𝕜 x z + inner_ 𝕜 y z
theorem InnerProductSpaceable.nat {𝕜 : Type u_1} [] {E : Type u_2} [] (n : ) (x : E) (y : E) :
inner_ 𝕜 (n x) y = n * inner_ 𝕜 x y
theorem InnerProductSpaceable.innerProp {𝕜 : Type u_1} [] {E : Type u_2} [] (r : 𝕜) :
noncomputable def InnerProductSpace.ofNorm (𝕜 : Type u_1) [] {E : Type u_2} [] (h : ∀ (x y : E), x + y * x + y + x - y * x - y = 2 * (x * x + y * y)) :

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

Equations
Instances For
theorem nonempty_innerProductSpace (𝕜 : Type u_1) [] (E : Type u_2) [] :

Fréchet–von Neumann–Jordan Theorem. A normed space E whose norm satisfies the parallelogram identity can be given a compatible inner product. Do casesI nonempty_innerProductSpace 𝕜 E to locally upgrade InnerProductSpaceable E to InnerProductSpace 𝕜 E.

Equations
• =