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

class InnerProductSpaceable (E : Type u_2) [NormedAddCommGroup E] : Prop

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.

• parallelogram_identity : ∀ (x y : E), ‖x + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖ = 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)

theorem InnerProductSpaceable.parallelogram_identity {E : Type u_2} [NormedAddCommGroup E] [self : InnerProductSpaceable E] (x : E) (y : E) : ‖x + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖ = 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)

theorem InnerProductSpace.toInnerProductSpaceable (𝕜 : Type u_1) [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : InnerProductSpaceable E

instance InnerProductSpace.toInnerProductSpaceable_ofReal {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : InnerProductSpaceable E

Equations

• ⋯ = ⋯

theorem InnerProductSpaceable.innerProp_neg_one {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] : InnerProductSpaceable.innerProp' E ↑(-1)

theorem Continuous.inner_ {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : ℝ → E} {g : ℝ → E} (hf : Continuous f) (hg : Continuous g) : Continuous fun (x : ℝ) => inner_ 𝕜 (f x) (g x)

theorem InnerProductSpaceable.inner_.norm_sq {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) : ‖x‖ ^ 2 = RCLike.re (inner_ 𝕜 x x)

theorem InnerProductSpaceable.inner_.conj_symm {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) (y : E) : (starRingEnd 𝕜) (inner_ 𝕜 y x) = inner_ 𝕜 x y

theorem InnerProductSpaceable.add_left {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpaceable E] (x : E) (y : E) (z : E) : inner_ 𝕜 (x + y) z = inner_ 𝕜 x z + inner_ 𝕜 y z

theorem InnerProductSpaceable.nat {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpaceable E] (n : ℕ) (x : E) (y : E) : inner_ 𝕜 (↑n • x) y = ↑n * inner_ 𝕜 x y

theorem InnerProductSpaceable.innerProp {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpaceable E] (r : 𝕜) : InnerProductSpaceable.innerProp' E r

noncomputable def InnerProductSpace.ofNorm (𝕜 : Type u_1) [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (h : ∀ (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.

Equations

• InnerProductSpace.ofNorm 𝕜 h = InnerProductSpace.mk ⋯ ⋯ ⋯ ⋯

theorem nonempty_innerProductSpace (𝕜 : Type u_1) [RCLike 𝕜] (E : Type u_2) [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpaceable E] : Nonempty (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. Do casesI nonempty_innerProductSpace 𝕜 E to locally upgrade InnerProductSpaceable E to InnerProductSpace 𝕜 E.

instance InnerProductSpaceable.to_uniformConvexSpace {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpaceable E] [NormedSpace ℝ E] : UniformConvexSpace E

Equations

• ⋯ = ⋯