Hilbert sum of a family of inner product spaces #
Given a family (G : ι → Type*) [Π i, InnerProductSpace 𝕜 (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 IsHilbertSum 𝕜 G V, where V : Π i, G i →ₗᵢ[𝕜] E, expressing that
V is an OrthogonalFamily and that the associated map lp G 2 →ₗᵢ[𝕜] E is surjective.
Main definitions #
OrthogonalFamily.linearIsometry: Given a Hilbert spaceE, a familyGof inner product spaces and a familyV : Π i, G i →ₗᵢ[𝕜] Eof isometric embeddings of theG iintoEwith mutually-orthogonal images, there is an induced isometric embedding of the Hilbert sum ofGintoE.IsHilbertSum: Given a Hilbert spaceE, a familyGof inner product spaces and a familyV : Π i, G i →ₗᵢ[𝕜] Eof isometric embeddings of theG iintoE,IsHilbertSum 𝕜 G Vmeans thatVis anOrthogonalFamilyand that the above linear isometry is surjective.IsHilbertSum.linearIsometryEquiv: If a Hilbert spaceEis a Hilbert sum of the inner product spacesG iwith respect to the familyV : Π i, G i →ₗᵢ[𝕜] E, then the correspondingOrthogonalFamily.linearIsometrycan be upgraded to aLinearIsometryEquiv.HilbertBasis: We define a Hilbert basis of a Hilbert spaceEto be a structure whose single fieldHilbertBasis.repris an isometric isomorphism ofEwithℓ²(ι, 𝕜)(i.e., the Hilbert sum ofιcopies of𝕜). This parallels the definition ofBasis, inLinearAlgebra.Basis, as an isomorphism of anR-module withι →₀ R.HilbertBasis.instCoeFun: More conventionally a Hilbert basis is thought of as a familyι → Eof vectors inEsatisfying certain properties (orthonormality, completeness). We obtain this interpretation of a Hilbert basisbby defining⇑b, of typeι → E, to be the image underb.reproflp.single 2 i (1:𝕜). This parallels the definitionBasis.coeFuninLinearAlgebra.Basis.HilbertBasis.mk: Make a Hilbert basis ofEfrom an orthonormal familyv : ι → Eof vectors inEwhose span is dense. This parallels the definitionBasis.mkinLinearAlgebra.Basis.HilbertBasis.mkOfOrthogonalEqBot: Make a Hilbert basis ofEfrom an orthonormal familyv : ι → Eof vectors inEwhose span has trivial orthogonal complement.
Main results #
lp.instInnerProductSpace: Construction of the inner product space instance on the Hilbert sumlp G 2. Note that from the fileAnalysis.Normed.Lp.lpSpace, the spacelp G 2already held a normed space instance (lp.normedSpace), and if eachG iis a Hilbert space (i.e., complete), thenlp G 2was already known to be complete (lp.completeSpace). So the work here is to define the inner product and show it is compatible.OrthogonalFamily.range_linearIsometry: Given a familyGof inner product spaces and a familyV : Π i, G i →ₗᵢ[𝕜] Eof isometric embeddings of theG iintoEwith mutually-orthogonal images, the image of the embeddingOrthogonalFamily.linearIsometryof the Hilbert sum ofGintoEis the closure of the span of the images of theG i.HilbertBasis.repr_apply_apply: Given a Hilbert basisbofE, the entryb.repr x iofx's representation inℓ²(ι, 𝕜)is the inner product⟪b i, x⟫.HilbertBasis.hasSum_repr: Given a Hilbert basisbofE, a vectorxinEcan be expressed as the "infinite linear combination"∑' i, b.repr x i • b iof the basis vectorsb i, with coefficients given by the entriesb.repr x iofx's representation inℓ²(ι, 𝕜).exists_hilbertBasis: A Hilbert space admits a Hilbert basis.
Keywords #
Hilbert space, Hilbert sum, l2, Hilbert basis, unitary equivalence, isometric isomorphism
ℓ²(ι, 𝕜) is the Hilbert space of square-summable functions ι → 𝕜, herein implemented
as lp (fun i : ι => 𝕜) 2.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Identification of a general Hilbert space E with a Hilbert sum #
A mutually orthogonal family of subspaces of E induce a linear isometry from lp 2 of the
subspaces into E.
Equations
- hV.linearIsometry = { toFun := fun (f : ↥(lp G 2)) => ∑' (i : ι), (V i) (↑f i), map_add' := ⋯, map_smul' := ⋯, norm_map' := ⋯ }
The canonical linear isometry from the lp 2 of a mutually orthogonal family of subspaces of
E into E, has range the closure of the span of the subspaces.
Given a family of Hilbert spaces G : ι → Type*, a Hilbert sum of G consists of a Hilbert
space E and an orthogonal family V : Π i, G i →ₗᵢ[𝕜] E such that the induced isometry
Φ : lp G 2 → E is surjective.
Keeping in mind that lp G 2 is "the" external Hilbert sum of G : ι → Type*, this is analogous
to DirectSum.IsInternal, except that we don't express it in terms of actual submodules.
- ofSurjective :: (
- OrthogonalFamily : OrthogonalFamily 𝕜 G V
The orthogonal family constituting the summands in the Hilbert sum.
- surjective_isometry : Function.Surjective ⇑⋯.linearIsometry
The isometry
lp G 2 → Einduced by the orthogonal family is surjective. - )
If V : Π i, G i →ₗᵢ[𝕜] E is an orthogonal family such that the supremum of the ranges of
V i is dense, then (E, V) is a Hilbert sum of G.
This is Orthonormal.isHilbertSum in the case of actual inclusions from subspaces.
A Hilbert sum (E, V) of G is canonically isomorphic to the Hilbert sum of G,
i.e lp G 2.
Note that this goes in the opposite direction from OrthogonalFamily.linearIsometry.
Equations
In the canonical isometric isomorphism between a Hilbert sum E of G and lp G 2,
a vector w : lp G 2 is the image of the infinite sum of the associated elements in E.
In the canonical isometric isomorphism between a Hilbert sum E of G and lp G 2,
a vector w : lp G 2 is the image of the infinite sum of the associated elements in E, and this
sum indeed converges.
In the canonical isometric isomorphism between a Hilbert sum E of G : ι → Type* and
lp G 2, an "elementary basis vector" in lp G 2 supported at i : ι is the image of the
associated element in E.
In the canonical isometric isomorphism between a Hilbert sum E of G : ι → Type* and
lp G 2, a finitely-supported vector in lp G 2 is the image of the associated finite sum of
elements of E.
In the canonical isometric isomorphism between a Hilbert sum E of G : ι → Type* and
lp G 2, a finitely-supported vector in lp G 2 is the image of the associated finite sum of
elements of E.
Given a total orthonormal family v : ι → E, E is a Hilbert sum of fun i : ι => 𝕜
relative to the family of linear isometries fun i k => k • v i.
Hilbert bases #
A Hilbert basis on ι for an inner product space E is an identification of E with the lp
space ℓ²(ι, 𝕜).
- ofRepr :: (
The linear isometric equivalence implementing identifying the Hilbert space with
ℓ².- )
Equations
- HilbertBasis.instInhabitedSubtypePreLpMemAddSubgroupLpOfNatENNReal = { default := { repr := LinearIsometryEquiv.refl 𝕜 ↥(lp (fun (i : ι) => 𝕜) 2) } }
b i is the ith basis vector.
Equations
- HilbertBasis.instFunLike = { coe := fun (b : HilbertBasis ι 𝕜 E) (i : ι) => b.repr.symm (lp.single 2 i 1), coe_injective' := ⋯ }
A finite Hilbert basis is an orthonormal basis.
Equations
An orthonormal family of vectors whose span is dense in the whole module is a Hilbert basis.
Equations
- HilbertBasis.mk hv hsp = { repr := ⋯.linearIsometryEquiv }
An orthonormal family of vectors whose span has trivial orthogonal complement is a Hilbert basis.
Equations
- HilbertBasis.mkOfOrthogonalEqBot hv hsp = HilbertBasis.mk hv ⋯
An orthonormal basis is a Hilbert basis.
Equations
- b.toHilbertBasis = HilbertBasis.mk ⋯ ⋯
A Hilbert space admits a Hilbert basis extending a given orthonormal subset.
A Hilbert space admits a Hilbert basis.