@[reducible, inline]

abbrev HilbertSpace.PreHilbertSpace (𝕜 : Type u_1) (H : Type u_2) [RCLike 𝕜] [SeminormedAddCommGroup H] : Type (max u_1 u_2)

A pre-Hilbert space is a vector space over $\mathbb{K} = \mathbb{R}, \mathbb{C}$ equipped with a Hermitian inner product $\langle \cdot, \cdot \rangle : H \times H \to \mathbb{K}$ satisfying linearity in the first argument, conjugate symmetry, and positive-definiteness. In Mathlib this is modeled by InnerProductSpace 𝕜 H.

theorem HilbertSpace.norm_eq_sqrt_inner {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_2} [SeminormedAddCommGroup H] [InnerProductSpace 𝕜 H] (x : H) : ‖x‖ = √(RCLike.re (inner 𝕜 x x))

Norm from inner product. In a (pre-)Hilbert space $H$, the norm of any $v \in H$ satisfies $\|v\| = \sqrt{\operatorname{Re}\,\langle v, v \rangle}$.

@[reducible]

noncomputable def HilbertSpace.normedAddCommGroupOfInnerProduct (𝕜 : Type u_1) (H : Type u_2) [RCLike 𝕜] [AddCommGroup H] [Module 𝕜 H] (c : InnerProductSpace.Core 𝕜 H) : NormedAddCommGroup H

An inner product (given as InnerProductSpace.Core data) induces a NormedAddCommGroup structure on $H$ via the norm $\|v\| = \langle v, v \rangle^{1/2}$. Hence, if $H$ is a pre-Hilbert space, then $\|\cdot\|$ is a genuine norm on $H$.

theorem HilbertSpace.cauchy_schwarz {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_2} [SeminormedAddCommGroup H] [InnerProductSpace 𝕜 H] (x y : H) : ‖inner 𝕜 x y‖ ≤ ‖x‖ * ‖y‖

Cauchy-Schwarz inequality. In a pre-Hilbert space $H$, for all $u, v \in H$ we have $|\langle u, v \rangle| \le \|u\|\,\|v\|$.

theorem HilbertSpace.parallelogram_law_iff (𝕜 : Type u_1) [RCLike 𝕜] {H : Type u_2} [NormedAddCommGroup H] [NormedSpace 𝕜 H] : (∀ (x y : H), ‖x + y‖ ^ 2 + ‖x - y‖ ^ 2 = 2 * (‖x‖ ^ 2 + ‖y‖ ^ 2)) ↔ Nonempty (InnerProductSpace 𝕜 H)

Parallelogram law (and its converse). A normed vector space $H$ over $\mathbb{K}$ satisfies the parallelogram law $$\|u+v\|^2 + \|u-v\|^2 = 2(\|u\|^2 + \|v\|^2) \quad \forall u, v \in H$$ if and only if $H$ is a pre-Hilbert space, i.e. there exists an inner product on $H$ inducing its norm.

theorem HilbertSpace.bessel_inequality {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_2} [SeminormedAddCommGroup H] [InnerProductSpace 𝕜 H] {ι : Type u_3} {v : ι → H} (hv : Orthonormal 𝕜 v) (x : H) : ∑' (i : ι), ‖inner 𝕜 x (v i)‖ ^ 2 ≤ ‖x‖ ^ 2

Bessel's inequality. Let $\{e_n\}$ be a (countable) orthonormal family in a pre-Hilbert space $H$. Then for every $u \in H$, $$\sum_n |\langle u, e_n \rangle|^2 \le \|u\|^2.$$

theorem HilbertSpace.inner_tendsto_of_tendsto {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x y : ℕ → E} {a b : E} (hx : Filter.Tendsto x Filter.atTop (nhds a)) (hy : Filter.Tendsto y Filter.atTop (nhds b)) : Filter.Tendsto (fun (n : ℕ) => inner 𝕜 (x n) (y n)) Filter.atTop (nhds (inner 𝕜 a b))

Continuity of the inner product. If $u_n \to a$ and $v_n \to b$ in a pre-Hilbert space, then $\langle u_n, v_n \rangle \to \langle a, b \rangle$.

theorem HilbertSpace.parseval_identity_hilbertBasis {𝕜 : Type u_3} [RCLike 𝕜] {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {ι : Type u_5} (b : HilbertBasis ι 𝕜 H) (u : H) : ∑' (i : ι), ‖inner 𝕜 u (b i)‖ ^ 2 = ‖u‖ ^ 2

Parseval's identity (Hilbert basis version). If $\{e_i\}_{i \in \iota}$ is a Hilbert basis of $H$, then for all $u \in H$, $$\sum_i |\langle u, e_i \rangle|^2 = \|u\|^2.$$

theorem HilbertSpace.parseval_identity {𝕜 : Type u_3} [RCLike 𝕜] {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {ι : Type u_5} [CompleteSpace H] {e : ι → H} (he : Orthonormal 𝕜 e) (hcomplete : ⊤ ≤ (Submodule.span 𝕜 (Set.range e)).topologicalClosure) (u : H) : ∑' (i : ι), ‖inner 𝕜 u (e i)‖ ^ 2 = ‖u‖ ^ 2

Parseval's identity. Let $H$ be a Hilbert space and let $\{e_i\}_{i \in \iota}$ be an orthonormal family whose span is dense in $H$ (i.e. an orthonormal basis). Then for all $u \in H$, $$\sum_i |\langle u, e_i \rangle|^2 = \|u\|^2.$$

theorem HilbertSpace.separable_hilbert_isomorphic_ell2 {𝕜 : Type u_3} [RCLike 𝕜] {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (b : HilbertBasis ℕ 𝕜 H) : Nonempty (H ≃ₗᵢ[𝕜] ↥(lp (fun (x : ℕ) => 𝕜) 2))

Separable Hilbert spaces are isometric to $\ell^2$. If $H$ is an infinite-dimensional separable Hilbert space (equivalently, if $H$ admits a countable Hilbert basis indexed by $\mathbb{N}$), then $H$ is isometrically linearly isomorphic to $\ell^2$, the space of square-summable sequences. In particular, the isomorphism preserves both norms and inner products.

theorem HilbertSpace.orthogonalProjection_is_projection {𝕜 : Type u_3} [RCLike 𝕜] {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (M : Submodule 𝕜 H) [M.HasOrthogonalProjection] : (∀ (x : H), M.orthogonalProjection ↑(M.orthogonalProjection x) = M.orthogonalProjection x) ∧ ‖M.starProjection‖ ≤ 1

Orthogonal projection onto a closed subspace. Let $H$ be a Hilbert space and let $W \subset H$ be a closed subspace. The orthogonal projection $\Pi_W : H \to H$ that sends $v = w + w^\perp$ (with $w \in W$ and $w^\perp \in W^\perp$) to $w$ is a projection operator: it is idempotent ($\Pi_W \circ \Pi_W = \Pi_W$) and has operator norm at most $1$.

theorem HilbertSpace.riesz_representation {𝕜 : Type u_3} [RCLike 𝕜] {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (f : H →L[𝕜] 𝕜) : ∃! y : H, (∀ (x : H), f x = inner 𝕜 y x) ∧ ‖f‖ = ‖y‖

Riesz Representation Theorem. Let $H$ be a Hilbert space. Then for every bounded linear functional $f \in H'$, there exists a unique $y \in H$ such that $f(x) = \langle y, x \rangle$ for all $x \in H$, and moreover $\|f\| = \|y\|$.

theorem HilbertSpace.separable_of_countable_hilbertBasis {𝕜 : Type u_3} [RCLike 𝕜] {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {ι : Type u_5} [Countable ι] (b : HilbertBasis ι 𝕜 H) : TopologicalSpace.SeparableSpace H

A Hilbert space with a countable orthonormal basis is separable. If a Hilbert space $H$ admits a Hilbert basis indexed by a countable set, then $H$ is separable: the closure of the $\mathbb{K}$-linear span of the basis contains a countable dense subset of $H$.