# mathlib3documentation

analysis.inner_product_space.l2_space

# Hilbert sum of a family of inner product spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 𝕜 G 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 𝕜 G 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#

theorem lp.summable_inner {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {G : ι Type u_4} [Π (i : ι), ] [Π (i : ι), (G i)] (f g : (lp G 2)) :
summable (λ (i : ι), has_inner.inner (f i) (g i))
@[protected, instance]
noncomputable def lp.inner_product_space {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {G : ι Type u_4} [Π (i : ι), ] [Π (i : ι), (G i)] :
(lp G 2)
Equations
theorem lp.inner_eq_tsum {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {G : ι Type u_4} [Π (i : ι), ] [Π (i : ι), (G i)] (f g : (lp G 2)) :
= ∑' (i : ι), has_inner.inner (f i) (g i)
theorem lp.has_sum_inner {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {G : ι Type u_4} [Π (i : ι), ] [Π (i : ι), (G i)] (f g : (lp G 2)) :
has_sum (λ (i : ι), has_inner.inner (f i) (g i)) g)
theorem lp.inner_single_left {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {G : ι Type u_4} [Π (i : ι), ] [Π (i : ι), (G i)] (i : ι) (a : G i) (f : (lp G 2)) :
has_inner.inner i a) f = (f i)
theorem lp.inner_single_right {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {G : ι Type u_4} [Π (i : ι), ] [Π (i : ι), (G i)] (i : ι) (a : G i) (f : (lp G 2)) :
i a) = has_inner.inner (f i) a

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

@[protected]
theorem orthogonal_family.summable_of_lp {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [cplt : complete_space E] {G : ι Type u_4} [Π (i : ι), ] [Π (i : ι), (G i)] {V : Π (i : ι), G i →ₗᵢ[𝕜] E} (hV : V) (f : (lp G 2)) :
summable (λ (i : ι), (V i) (f i))
@[protected]
noncomputable def orthogonal_family.linear_isometry {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [cplt : complete_space E] {G : ι Type u_4} [Π (i : ι), ] [Π (i : ι), (G i)] {V : Π (i : ι), G i →ₗᵢ[𝕜] E} (hV : V) :
(lp G 2) →ₗᵢ[𝕜] E

A mutually orthogonal family of subspaces of E induce a linear isometry from lp 2 of the subspaces into E.

Equations
@[protected]
theorem orthogonal_family.linear_isometry_apply {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [cplt : complete_space E] {G : ι Type u_4} [Π (i : ι), ] [Π (i : ι), (G i)] {V : Π (i : ι), G i →ₗᵢ[𝕜] E} (hV : V) (f : (lp G 2)) :
(hV.linear_isometry) f = ∑' (i : ι), (V i) (f i)
@[protected]
theorem orthogonal_family.has_sum_linear_isometry {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [cplt : complete_space E] {G : ι Type u_4} [Π (i : ι), ] [Π (i : ι), (G i)] {V : Π (i : ι), G i →ₗᵢ[𝕜] E} (hV : V) (f : (lp G 2)) :
has_sum (λ (i : ι), (V i) (f i)) ((hV.linear_isometry) f)
@[protected, simp]
theorem orthogonal_family.linear_isometry_apply_single {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [cplt : complete_space E] {G : ι Type u_4} [Π (i : ι), ] [Π (i : ι), (G i)] {V : Π (i : ι), G i →ₗᵢ[𝕜] E} (hV : V) {i : ι} (x : G i) :
(hV.linear_isometry) i x) = (V i) x
@[protected, simp]
theorem orthogonal_family.linear_isometry_apply_dfinsupp_sum_single {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [cplt : complete_space E] {G : ι Type u_4} [Π (i : ι), ] [Π (i : ι), (G i)] {V : Π (i : ι), G i →ₗᵢ[𝕜] E} (hV : V) (W₀ : Π₀ (i : ι), G i) :
(hV.linear_isometry) (W₀.sum (lp.single 2)) = W₀.sum (λ (i : ι), (V i))
@[protected]
theorem orthogonal_family.range_linear_isometry {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [cplt : complete_space E] {G : ι Type u_4} [Π (i : ι), ] [Π (i : ι), (G i)] {V : Π (i : ι), G i →ₗᵢ[𝕜] E} (hV : V) [ (i : ι), complete_space (G i)] :

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.

structure is_hilbert_sum {ι : Type u_1} (𝕜 : Type u_2) [is_R_or_C 𝕜] {E : Type u_3} [ E] [cplt : complete_space E] (G : ι Type u_4) [Π (i : ι), ] [Π (i : ι), (G i)] (V : Π (i : ι), G i →ₗᵢ[𝕜] E) :
Prop
• orthogonal_family : V
• surjective_isometry :

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 direct_sum.is_internal, except that we don't express it in terms of actual submodules.

theorem is_hilbert_sum.mk {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [cplt : complete_space E] {G : ι Type u_4} [Π (i : ι), ] [Π (i : ι), (G i)] {V : Π (i : ι), G i →ₗᵢ[𝕜] E} [ (i : ι), complete_space (G i)] (hVortho : V) (hVtotal : ( (i : ι), .topological_closure) :
V

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.

theorem is_hilbert_sum.mk_internal {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [cplt : complete_space E] (F : ι E) [ (i : ι), complete_space (F i)] (hFortho : (λ (i : ι), (F i)) (λ (i : ι), (F i).subtypeₗᵢ)) (hFtotal : ( (i : ι), F i).topological_closure) :
(λ (i : ι), (F i)) (λ (i : ι), (F i).subtypeₗᵢ)

This is orthogonal_family.is_hilbert_sum in the case of actual inclusions from subspaces.

noncomputable def is_hilbert_sum.linear_isometry_equiv {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [cplt : complete_space E] {G : ι Type u_4} [Π (i : ι), ] [Π (i : ι), (G i)] {V : Π (i : ι), G i →ₗᵢ[𝕜] E} (hV : V) :
E ≃ₗᵢ[𝕜] (lp G 2)

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 orthogonal_family.linear_isometry.

Equations
@[protected]
theorem is_hilbert_sum.linear_isometry_equiv_symm_apply {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [cplt : complete_space E] {G : ι Type u_4} [Π (i : ι), ] [Π (i : ι), (G i)] {V : Π (i : ι), G i →ₗᵢ[𝕜] E} (hV : V) (w : (lp G 2)) :
(hV.linear_isometry_equiv.symm) w = ∑' (i : ι), (V i) (w i)

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.

@[protected]
theorem is_hilbert_sum.has_sum_linear_isometry_equiv_symm {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [cplt : complete_space E] {G : ι Type u_4} [Π (i : ι), ] [Π (i : ι), (G i)] {V : Π (i : ι), G i →ₗᵢ[𝕜] E} (hV : V) (w : (lp G 2)) :
has_sum (λ (i : ι), (V i) (w i)) ((hV.linear_isometry_equiv.symm) w)

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.

@[protected, simp]
theorem is_hilbert_sum.linear_isometry_equiv_symm_apply_single {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [cplt : complete_space E] {G : ι Type u_4} [Π (i : ι), ] [Π (i : ι), (G i)] {V : Π (i : ι), G i →ₗᵢ[𝕜] E} (hV : V) {i : ι} (x : G i) :

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.

@[protected, simp]
theorem is_hilbert_sum.linear_isometry_equiv_symm_apply_dfinsupp_sum_single {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [cplt : complete_space E] {G : ι Type u_4} [Π (i : ι), ] [Π (i : ι), (G i)] {V : Π (i : ι), G i →ₗᵢ[𝕜] E} (hV : V) (W₀ : Π₀ (i : ι), G i) :
(hV.linear_isometry_equiv.symm) (W₀.sum (lp.single 2)) = W₀.sum (λ (i : ι), (V i))

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.

@[protected, simp]
theorem is_hilbert_sum.linear_isometry_equiv_apply_dfinsupp_sum_single {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [cplt : complete_space E] {G : ι Type u_4} [Π (i : ι), ] [Π (i : ι), (G i)] {V : Π (i : ι), G i →ₗᵢ[𝕜] E} (hV : V) (W₀ : Π₀ (i : ι), G i) :
((hV.linear_isometry_equiv) (W₀.sum (λ (i : ι), (V i)))) = W₀

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.

theorem orthonormal.is_hilbert_sum {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [cplt : complete_space E] {v : ι E} (hv : v) (hsp : ) :
(λ (i : ι), 𝕜) (λ (i : ι),

Given a total orthonormal family v : ι → E, E is a Hilbert sum of λ i : ι, 𝕜 relative to the family of linear isometries λ i, λ k, k • v i.

theorem submodule.is_hilbert_sum_orthogonal {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [cplt : complete_space E] (K : E) [hK : complete_space K] :
(λ (b : bool), (cond b K K)) (λ (b : bool), (cond b K K).subtypeₗᵢ)

### Hilbert bases #

structure hilbert_basis (ι : Type u_1) (𝕜 : Type u_2) [is_R_or_C 𝕜] (E : Type u_3) [ E] :
Type (max u_1 u_2 u_3)

A Hilbert basis on ι for an inner product space E is an identification of E with the lp space ℓ²(ι, 𝕜).

Instances for hilbert_basis
@[protected, instance]
noncomputable def hilbert_basis.inhabited {𝕜 : Type u_2} [is_R_or_C 𝕜] {ι : Type u_1} :
inhabited 𝕜 (lp (λ (i : ι), 𝕜) 2))
Equations
@[protected, instance]
noncomputable def hilbert_basis.has_coe_to_fun {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] :
has_coe_to_fun 𝕜 E) (λ (_x : E), ι E)

b i is the ith basis vector.

Equations
@[protected, simp]
theorem hilbert_basis.repr_symm_single {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] (b : E) (i : ι) :
(b.repr.symm) i 1) = b i
@[protected, simp]
theorem hilbert_basis.repr_self {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] (b : E) (i : ι) :
(b.repr) (b i) = i 1
@[protected]
theorem hilbert_basis.repr_apply_apply {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] (b : E) (v : E) (i : ι) :
((b.repr) v) i = has_inner.inner (b i) v
@[protected, simp]
theorem hilbert_basis.orthonormal {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] (b : E) :
b
@[protected]
theorem hilbert_basis.has_sum_repr_symm {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] (b : E) (f : (lp (λ (i : ι), 𝕜) 2)) :
has_sum (λ (i : ι), f i b i) ((b.repr.symm) f)
@[protected]
theorem hilbert_basis.has_sum_repr {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] (b : E) (x : E) :
has_sum (λ (i : ι), ((b.repr) x) i b i) x
@[protected, simp]
theorem hilbert_basis.dense_span {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] (b : E) :
@[protected]
theorem hilbert_basis.has_sum_inner_mul_inner {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] (b : E) (x y : E) :
has_sum (λ (i : ι), (b i) * has_inner.inner (b i) y) y)
@[protected]
theorem hilbert_basis.summable_inner_mul_inner {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] (b : E) (x y : E) :
summable (λ (i : ι), (b i) * has_inner.inner (b i) y)
@[protected]
theorem hilbert_basis.tsum_inner_mul_inner {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] (b : E) (x y : E) :
∑' (i : ι), (b i) * has_inner.inner (b i) y =
@[protected]
noncomputable def hilbert_basis.to_orthonormal_basis {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [fintype ι] (b : E) :
E

A finite Hilbert basis is an orthonormal basis.

Equations
@[simp]
theorem hilbert_basis.coe_to_orthonormal_basis {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [fintype ι] (b : E) :
@[protected]
theorem hilbert_basis.has_sum_orthogonal_projection {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] {U : E} (b : U) (x : E) :
has_sum (λ (i : ι), has_inner.inner (b i) x b i) x)
theorem hilbert_basis.finite_spans_dense {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] (b : E) :
@[protected]
noncomputable def hilbert_basis.mk {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [cplt : complete_space E] {v : ι E} (hv : v) (hsp : ) :
E

An orthonormal family of vectors whose span is dense in the whole module is a Hilbert basis.

Equations
theorem orthonormal.linear_isometry_equiv_symm_apply_single_one {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [cplt : complete_space E] {v : ι E} (hv : v) (h : ) (i : ι) :
@[protected, simp]
theorem hilbert_basis.coe_mk {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [cplt : complete_space E] {v : ι E} (hv : v) (hsp : ) :
hsp) = v
@[protected]
noncomputable def hilbert_basis.mk_of_orthogonal_eq_bot {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [cplt : complete_space E] {v : ι E} (hv : v) (hsp : (set.range v)) = ) :
E

An orthonormal family of vectors whose span has trivial orthogonal complement is a Hilbert basis.

Equations
@[protected, simp]
theorem hilbert_basis.coe_of_orthogonal_eq_bot_mk {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [cplt : complete_space E] {v : ι E} (hv : v) (hsp : (set.range v)) = ) :
= v
@[protected]
noncomputable def orthonormal_basis.to_hilbert_basis {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [cplt : complete_space E] [fintype ι] (b : E) :
E

An orthonormal basis is an Hilbert basis.

Equations
@[simp]
theorem orthonormal_basis.coe_to_hilbert_basis {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [cplt : complete_space E] [fintype ι] (b : E) :
theorem orthonormal.exists_hilbert_basis_extension {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [cplt : complete_space E] {s : set E} (hs : coe) :
(w : set E) (b : E), s w

A Hilbert space admits a Hilbert basis extending a given orthonormal subset.

theorem exists_hilbert_basis (𝕜 : Type u_2) [is_R_or_C 𝕜] (E : Type u_3) [ E] [cplt : complete_space E] :
(w : set E) (b : E),

A Hilbert space admits a Hilbert basis.