Hilbert sum of a family of inner product spaces #

Given a family (G : ι → Type*) [Π i, inner_product_space 𝕜 (G i)] of inner product spaces, this file equips lp G 2 with an inner product space structure, where lp G 2 consists of those dependent functions f : Π i, G i for which ∑' i, ‖f i‖ ^ 2, the sum of the norms-squared, is summable. This construction is sometimes called the Hilbert sum of the family G. By choosing G to be ι → 𝕜, the Hilbert space ℓ²(ι, 𝕜) may be seen as a special case of this construction.

We also define a predicate is_hilbert_sum 𝕜 E V, where V : Π i, G i →ₗᵢ[𝕜] E, expressing that V is an orthogonal_family and that the associated map lp G 2 →ₗᵢ[𝕜] E is surjective.

Main definitions #

• orthogonal_family.linear_isometry: Given a Hilbert space E, a family G of inner product spaces and a family V : Π i, G i →ₗᵢ[𝕜] E of isometric embeddings of the G i into E with mutually-orthogonal images, there is an induced isometric embedding of the Hilbert sum of G into E.

• is_hilbert_sum: Given a Hilbert space E, a family G of inner product spaces and a family V : Π i, G i →ₗᵢ[𝕜] E of isometric embeddings of the G i into E, is_hilbert_sum 𝕜 E V means that V is an orthogonal_family and that the above linear isometry is surjective.

• is_hilbert_sum.linear_isometry_equiv: If a Hilbert space E is a Hilbert sum of the inner product spaces G i with respect to the family V : Π i, G i →ₗᵢ[𝕜] E, then the corresponding orthogonal_family.linear_isometry can be upgraded to a linear_isometry_equiv.

• hilbert_basis: We define a Hilbert basis of a Hilbert space E to be a structure whose single field hilbert_basis.repr is an isometric isomorphism of E with ℓ²(ι, 𝕜) (i.e., the Hilbert sum of ι copies of 𝕜). This parallels the definition of basis, in linear_algebra.basis, as an isomorphism of an R-module with ι →₀ R.

• hilbert_basis.has_coe_to_fun: More conventionally a Hilbert basis is thought of as a family ι → E of vectors in E satisfying certain properties (orthonormality, completeness). We obtain this interpretation of a Hilbert basis b by defining ⇑b, of type ι → E, to be the image under b.repr of lp.single 2 i (1:𝕜). This parallels the definition basis.has_coe_to_fun in linear_algebra.basis.

• hilbert_basis.mk: Make a Hilbert basis of E from an orthonormal family v : ι → E of vectors in E whose span is dense. This parallels the definition basis.mk in linear_algebra.basis.

• hilbert_basis.mk_of_orthogonal_eq_bot: Make a Hilbert basis of E from an orthonormal family v : ι → E of vectors in E whose span has trivial orthogonal complement.

Main results #

• lp.inner_product_space: Construction of the inner product space instance on the Hilbert sum lp G 2. Note that from the file analysis.normed_space.lp_space, the space lp G 2 already held a normed space instance (lp.normed_space), and if each G i is a Hilbert space (i.e., complete), then lp G 2 was already known to be complete (lp.complete_space). So the work here is to define the inner product and show it is compatible.

• orthogonal_family.range_linear_isometry: Given a family G of inner product spaces and a family V : Π i, G i →ₗᵢ[𝕜] E of isometric embeddings of the G i into E with mutually-orthogonal images, the image of the embedding orthogonal_family.linear_isometry of the Hilbert sum of G into E is the closure of the span of the images of the G i.

• hilbert_basis.repr_apply_apply: Given a Hilbert basis b of E, the entry b.repr x i of x's representation in ℓ²(ι, 𝕜) is the inner product ⟪b i, x⟫.

• hilbert_basis.has_sum_repr: Given a Hilbert basis b of E, a vector x in E can be expressed as the "infinite linear combination" ∑' i, b.repr x i • b i of the basis vectors b i, with coefficients given by the entries b.repr x i of x's representation in ℓ²(ι, 𝕜).

• exists_hilbert_basis: A Hilbert space admits a Hilbert basis.

Keywords #

Hilbert space, Hilbert sum, l2, Hilbert basis, unitary equivalence, isometric isomorphism

Inner product space structure on lp G 2 #

Identification of a general Hilbert space E with a Hilbert sum #

Hilbert bases #