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.
Main definitions #
-
orthogonal_family.linear_isometry
: Given a Hilbert spaceE
, a familyG
of inner product spaces and a familyV : ฮ i, G i โโแตข[๐] E
of isometric embeddings of theG i
intoE
with mutually-orthogonal images, there is an induced isometric embedding of the Hilbert sum ofG
intoE
. -
orthogonal_family.linear_isometry_equiv
: Given a Hilbert spaceE
, a familyG
of inner product spaces and a familyV : ฮ i, G i โโแตข[๐] E
of isometric embeddings of theG i
intoE
with mutually-orthogonal images whose span is dense inE
, there is an induced isometric isomorphism of the Hilbert sum ofG
withE
. -
hilbert_basis
: We define a Hilbert basis of a Hilbert spaceE
to be a structure whose single fieldhilbert_basis.repr
is an isometric isomorphism ofE
withโยฒ(ฮน, ๐)
(i.e., the Hilbert sum ofฮน
copies of๐
). This parallels the definition ofbasis
, inlinear_algebra.basis
, as an isomorphism of anR
-module withฮน โโ R
. -
hilbert_basis.has_coe_to_fun
: More conventionally a Hilbert basis is thought of as a familyฮน โ E
of vectors inE
satisfying certain properties (orthonormality, completeness). We obtain this interpretation of a Hilbert basisb
by definingโb
, of typeฮน โ E
, to be the image underb.repr
oflp.single 2 i (1:๐)
. This parallels the definitionbasis.has_coe_to_fun
inlinear_algebra.basis
. -
hilbert_basis.mk
: Make a Hilbert basis ofE
from an orthonormal familyv : ฮน โ E
of vectors inE
whose span is dense. This parallels the definitionbasis.mk
inlinear_algebra.basis
. -
hilbert_basis.mk_of_orthogonal_eq_bot
: Make a Hilbert basis ofE
from an orthonormal familyv : ฮน โ E
of vectors inE
whose span has trivial orthogonal complement.
Main results #
-
lp.inner_product_space
: Construction of the inner product space instance on the Hilbert sumlp G 2
. Note that from the fileanalysis.normed_space.lp_space
, the spacelp G 2
already held a normed space instance (lp.normed_space
), and if eachG i
is a Hilbert space (i.e., complete), thenlp 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 familyG
of inner product spaces and a familyV : ฮ i, G i โโแตข[๐] E
of isometric embeddings of theG i
intoE
with mutually-orthogonal images, the image of the embeddingorthogonal_family.linear_isometry
of the Hilbert sum ofG
intoE
is the closure of the span of the images of theG i
. -
hilbert_basis.repr_apply_apply
: Given a Hilbert basisb
ofE
, the entryb.repr x i
ofx
's representation inโยฒ(ฮน, ๐)
is the inner productโชb i, xโซ
. -
hilbert_basis.has_sum_repr
: Given a Hilbert basisb
ofE
, a vectorx
inE
can be expressed as the "infinite linear combination"โ' i, b.repr x i โข b i
of the basis vectorsb i
, with coefficients given by the entriesb.repr x i
ofx
'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
Equations
- lp.inner_product_space = {to_normed_group := lp.normed_group fact_one_le_two_ennreal, to_normed_space := {to_module := normed_space.to_module lp.normed_space, norm_smul_le := _}, to_has_inner := {inner := ฮป (f g : โฅ(lp G 2)), โ' (i : ฮน), has_inner.inner (โf i) (โg i)}, norm_sq_eq_inner := _, conj_sym := _, add_left := _, smul_left := _}
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
.
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.
A mutually orthogonal family of complete subspaces of E
, whose range is dense in E
, induces
a isometric isomorphism from E to lp 2
of the subspaces.
Note that this goes in the opposite direction from orthogonal_family.linear_isometry
.
Equations
In the canonical isometric isomorphism E โโแตข[๐] lp G 2
induced by an orthogonal family G
,
a vector w : lp G 2
is the image of the infinite sum of the associated elements in E
.
In the canonical isometric isomorphism E โโแตข[๐] lp G 2
induced by an orthogonal family G
,
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 E โโแตข[๐] lp G 2
induced by an ฮน
-indexed orthogonal
family G
, 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 E โโแตข[๐] lp G 2
induced by an ฮน
-indexed orthogonal
family G
, 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 E โโแตข[๐] lp G 2
induced by an ฮน
-indexed orthogonal
family G
, a finitely-supported vector in lp G 2
is the image of the associated finite sum of
elements of E
.
Hilbert bases #
- repr : E โโแตข[๐] โฅ(lp (ฮป (i : ฮน), ๐) 2)
A Hilbert basis on ฮน
for an inner product space E
is an identification of E
with the lp
space โยฒ(ฮน, ๐)
.
Instances for hilbert_basis
- hilbert_basis.has_sizeof_inst
- hilbert_basis.inhabited
- hilbert_basis.has_coe_to_fun
Equations
- hilbert_basis.inhabited = {default := {repr := linear_isometry_equiv.refl ๐ โฅ(lp (ฮป (i : ฮน), ๐) 2) normed_space.to_module}}
b i
is the i
th basis vector.
Equations
- hilbert_basis.has_coe_to_fun = {coe := ฮป (b : hilbert_basis ฮน ๐ E) (i : ฮน), โ(b.repr.symm) (lp.single 2 i 1)}
An orthonormal family of vectors whose span is dense in the whole module is a Hilbert basis.
Equations
- hilbert_basis.mk hv hsp = {repr := _.linear_isometry_equiv _}
An orthonormal family of vectors whose span has trivial orthogonal complement is a Hilbert basis.
Equations
- hilbert_basis.mk_of_orthogonal_eq_bot hv hsp = hilbert_basis.mk hv _
A Hilbert space admits a Hilbert basis extending a given orthonormal subset.
A Hilbert space admits a Hilbert basis.