# mathlib3documentation

analysis.inner_product_space.of_norm

# Inner product space derived from a norm #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines an inner_product_space 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 #

• inner_product_space.of_norm: 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.inner_product_space.basic.

## Tags #

inner product space, Hilbert space, norm

@[class]
structure inner_product_spaceable (E : Type u_2)  :
Prop

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

Instances of this typeclass
theorem inner_product_space.to_inner_product_spaceable (𝕜 : Type u_1) [is_R_or_C 𝕜] {E : Type u_2} [ E] :
@[protected, instance]
theorem inner_product_spaceable.inner_prop_neg_one {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] :
inner_prop E -1
theorem inner_product_spaceable.continuous.inner_ {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] {f g : E} (hf : continuous f) (hg : continuous g) :
continuous (λ (x : ), inner_ 𝕜 (f x) (g x))
theorem inner_product_spaceable.inner_.norm_sq {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] (x : E) :
x ^ 2 = is_R_or_C.re (inner_ 𝕜 x x)
theorem inner_product_spaceable.inner_.conj_symm {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] (x y : E) :
(inner_ 𝕜 y x) = inner_ 𝕜 x y
theorem inner_product_spaceable.add_left {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] (x y z : E) :
inner_ 𝕜 (x + y) z = inner_ 𝕜 x z + inner_ 𝕜 y z
theorem inner_product_spaceable.nat {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] (n : ) (x y : E) :
inner_ 𝕜 (n x) y = n * inner_ 𝕜 x y
theorem inner_product_spaceable.inner_prop {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] (r : 𝕜) :
inner_prop E r
noncomputable def inner_product_space.of_norm (𝕜 : Type u_1) [is_R_or_C 𝕜] {E : Type u_2} [ E] (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
theorem nonempty_inner_product_space (𝕜 : Type u_1) [is_R_or_C 𝕜] (E : Type u_2) [ 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_inner_product_space 𝕜 E to locally upgrade inner_product_spaceable E to inner_product_space 𝕜 E.

@[protected, instance]