Separable Hilbert spaces

TheoremA Hilbert space with a countable orthonormal basis is separable#✓fully proved

If H admits a Hilbert basis indexed by a countable type, then H is separable. No completeness hypothesis is needed: it is the density of the span of the basis, not completeness, that is used.

theorem separableSpace_of_countable_hilbertBasis {ι : Type*} [Countable ι]
    (b : HilbertBasis ι 𝕜 H) : SeparableSpace H

Used by 1

Used byRolewicz's theorem

TheoremAn orthonormal family in a separable space is countable#✓fully proved

Let \(H\) be a separable inner product space over \(\mathbb{R}\) or \(\mathbb{C}\). If \((v_i)_{i \in \iota}\) is an orthonormal family in \(H\), then the index set \(\iota\) is countable.

Distinct orthonormal vectors are at distance \(\sqrt{2}\), so the open balls of radius \(1/2\) around them are pairwise disjoint.

theorem countable_of_orthonormal [SeparableSpace H] {ι : Type*} {v : ι → H}
    (hv : Orthonormal 𝕜 v) : Countable ι

Used by 1

Used byA separable Hilbert space admits a countable Hilbert basis

TheoremA separable Hilbert space admits a countable Hilbert basis#✓fully proved

Let \(H\) be a separable Hilbert space over \(\mathbb{R}\) or \(\mathbb{C}\). Then \(H\) has a Hilbert basis \((e_i)_{i \in \iota}\) (an orthonormal family whose linear span is dense in \(H\)) indexed by a countable set \(\iota\).

theorem exists_countable_hilbertBasis [CompleteSpace H] [SeparableSpace H] :
    ∃ (ι : Type u) (_ : Countable ι), Nonempty (HilbertBasis ι 𝕜 H)

Uses 1 · Used by 1

Proof usesAn orthonormal family in a separable space is countable

Used byAn infinite-dimensional separable Hilbert space admits a Hilbert basis indexed by \(\mathbb{N}\)

TheoremAn infinite-dimensional separable Hilbert space admits a Hilbert basis indexed by \(\mathbb{N}\)#✓fully proved

An infinite-dimensional separable Hilbert space admits a Hilbert basis indexed by \(\mathbb{N}\). Let \(H\) be a separable Hilbert space over \(\mathbb{R}\) or \(\mathbb{C}\) that is not finite-dimensional. Then \(H\) has a Hilbert basis \((e_n)_{n \in \mathbb{N}}\) indexed by the natural numbers.

A countable Hilbert basis of \(H\) has an infinite index set, which is therefore in bijection with \(\mathbb{N}\); reindexing along this bijection gives the basis.

theorem exists_hilbertBasis_nat [CompleteSpace H] [SeparableSpace H]
    (hInf : ¬FiniteDimensional 𝕜 H) : Nonempty (HilbertBasis ℕ 𝕜 H)

Uses 1 · Used by 1

Proof usesA separable Hilbert space admits a countable Hilbert basis

Used byAn infinite-dimensional separable Hilbert space is isometrically isomorphic to \(\ell^2\)

TheoremAn infinite-dimensional separable Hilbert space is isometrically isomorphic to \(\ell^2\)#✓fully proved

An infinite-dimensional separable Hilbert space is isometrically isomorphic to \(\ell^2\). Let \(H\) be a separable Hilbert space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\) that is not finite-dimensional. Then there is a \(\mathbb{K}\)-linear isometric isomorphism from \(H\) onto \(\ell^2(\mathbb{N}, \mathbb{K})\), the space of square-summable sequences in \(\mathbb{K}\).

The isomorphism sends a vector to its coefficients with respect to a Hilbert basis of \(H\) indexed by \(\mathbb{N}\), so it preserves norms and inner products.

theorem separable_hilbert_iso_l2 [CompleteSpace H] [SeparableSpace H]
    (hInf : ¬FiniteDimensional 𝕜 H) :
    Nonempty (H ≃ₗᵢ[𝕜] lp (fun _ : ℕ => 𝕜) 2)

Uses 1

Proof usesAn infinite-dimensional separable Hilbert space admits a Hilbert basis indexed by \(\mathbb{N}\)

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.