mathlib documentation

analysis.inner_product_space.l2_space

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 #

Main results #

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 : ι), inner_product_space 𝕜 (G i)] (f g : (lp G 2)) :
summable (λ (i : ι), has_inner.inner (f i) (g i))
theorem lp.inner_eq_tsum {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {G : ι Type u_4} [Π (i : ι), inner_product_space 𝕜 (G i)] (f g : (lp G 2)) :
has_inner.inner f g = ∑' (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 : ι), inner_product_space 𝕜 (G i)] (f g : (lp G 2)) :
has_sum (λ (i : ι), has_inner.inner (f i) (g i)) (has_inner.inner f g)
theorem lp.inner_single_left {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {G : ι Type u_4} [Π (i : ι), inner_product_space 𝕜 (G i)] (i : ι) (a : G i) (f : (lp G 2)) :
theorem lp.inner_single_right {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {G : ι Type u_4} [Π (i : ι), inner_product_space 𝕜 (G i)] (i : ι) (a : G i) (f : (lp G 2)) :

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} [inner_product_space 𝕜 E] [cplt : complete_space E] {G : ι Type u_4} [Π (i : ι), inner_product_space 𝕜 (G i)] {V : Π (i : ι), G i →ₗᵢ[𝕜] E} (hV : orthogonal_family 𝕜 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} [inner_product_space 𝕜 E] [cplt : complete_space E] {G : ι Type u_4} [Π (i : ι), inner_product_space 𝕜 (G i)] {V : Π (i : ι), G i →ₗᵢ[𝕜] E} (hV : orthogonal_family 𝕜 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} [inner_product_space 𝕜 E] [cplt : complete_space E] {G : ι Type u_4} [Π (i : ι), inner_product_space 𝕜 (G i)] {V : Π (i : ι), G i →ₗᵢ[𝕜] E} (hV : orthogonal_family 𝕜 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} [inner_product_space 𝕜 E] [cplt : complete_space E] {G : ι Type u_4} [Π (i : ι), inner_product_space 𝕜 (G i)] {V : Π (i : ι), G i →ₗᵢ[𝕜] E} (hV : orthogonal_family 𝕜 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} [inner_product_space 𝕜 E] [cplt : complete_space E] {G : ι Type u_4} [Π (i : ι), inner_product_space 𝕜 (G i)] {V : Π (i : ι), G i →ₗᵢ[𝕜] E} (hV : orthogonal_family 𝕜 V) {i : ι} (x : G i) :
(hV.linear_isometry) (lp.single 2 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} [inner_product_space 𝕜 E] [cplt : complete_space E] {G : ι Type u_4} [Π (i : ι), inner_product_space 𝕜 (G i)] {V : Π (i : ι), G i →ₗᵢ[𝕜] E} (hV : orthogonal_family 𝕜 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} [inner_product_space 𝕜 E] [cplt : complete_space E] {G : ι Type u_4} [Π (i : ι), inner_product_space 𝕜 (G i)] {V : Π (i : ι), G i →ₗᵢ[𝕜] E} (hV : orthogonal_family 𝕜 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) [inner_product_space 𝕜 E] [cplt : complete_space E] {G : ι Type u_4} [Π (i : ι), inner_product_space 𝕜 (G i)] (V : Π (i : ι), G i →ₗᵢ[𝕜] E) :
Prop

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} [inner_product_space 𝕜 E] [cplt : complete_space E] {G : ι Type u_4} [Π (i : ι), inner_product_space 𝕜 (G i)] {V : Π (i : ι), G i →ₗᵢ[𝕜] E} [ (i : ι), complete_space (G i)] (hVortho : orthogonal_family 𝕜 V) (hVtotal : ( (i : ι), linear_map.range (V i).to_linear_map).topological_closure) :

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} [inner_product_space 𝕜 E] [cplt : complete_space E] (F : ι submodule 𝕜 E) [ (i : ι), complete_space (F i)] (hFortho : orthogonal_family 𝕜 (λ (i : ι), (F i).subtypeₗᵢ)) (hFtotal : ( (i : ι), F i).topological_closure) :
is_hilbert_sum 𝕜 E (λ (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} [inner_product_space 𝕜 E] [cplt : complete_space E] {G : ι Type u_4} [Π (i : ι), inner_product_space 𝕜 (G i)] {V : Π (i : ι), G i →ₗᵢ[𝕜] E} (hV : is_hilbert_sum 𝕜 E 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} [inner_product_space 𝕜 E] [cplt : complete_space E] {G : ι Type u_4} [Π (i : ι), inner_product_space 𝕜 (G i)] {V : Π (i : ι), G i →ₗᵢ[𝕜] E} (hV : is_hilbert_sum 𝕜 E 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} [inner_product_space 𝕜 E] [cplt : complete_space E] {G : ι Type u_4} [Π (i : ι), inner_product_space 𝕜 (G i)] {V : Π (i : ι), G i →ₗᵢ[𝕜] E} (hV : is_hilbert_sum 𝕜 E 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} [inner_product_space 𝕜 E] [cplt : complete_space E] {G : ι Type u_4} [Π (i : ι), inner_product_space 𝕜 (G i)] {V : Π (i : ι), G i →ₗᵢ[𝕜] E} (hV : is_hilbert_sum 𝕜 E 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} [inner_product_space 𝕜 E] [cplt : complete_space E] {G : ι Type u_4} [Π (i : ι), inner_product_space 𝕜 (G i)] {V : Π (i : ι), G i →ₗᵢ[𝕜] E} (hV : is_hilbert_sum 𝕜 E 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} [inner_product_space 𝕜 E] [cplt : complete_space E] {G : ι Type u_4} [Π (i : ι), inner_product_space 𝕜 (G i)] {V : Π (i : ι), G i →ₗᵢ[𝕜] E} (hV : is_hilbert_sum 𝕜 E 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} [inner_product_space 𝕜 E] [cplt : complete_space E] {v : ι E} (hv : orthonormal 𝕜 v) (hsp : (submodule.span 𝕜 (set.range v)).topological_closure) :
is_hilbert_sum 𝕜 E (λ (i : ι), linear_isometry.to_span_singleton 𝕜 E _)

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} [inner_product_space 𝕜 E] [cplt : complete_space E] (K : submodule 𝕜 E) [hK : complete_space K] :
is_hilbert_sum 𝕜 E (λ (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) [inner_product_space 𝕜 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 (hilbert_basis ι 𝕜 (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} [inner_product_space 𝕜 E] :
has_coe_to_fun (hilbert_basis ι 𝕜 E) (λ (_x : hilbert_basis ι 𝕜 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} [inner_product_space 𝕜 E] (b : hilbert_basis ι 𝕜 E) (i : ι) :
(b.repr.symm) (lp.single 2 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} [inner_product_space 𝕜 E] (b : hilbert_basis ι 𝕜 E) (i : ι) :
(b.repr) (b i) = lp.single 2 i 1
@[protected]
theorem hilbert_basis.repr_apply_apply {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [inner_product_space 𝕜 E] (b : hilbert_basis ι 𝕜 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} [inner_product_space 𝕜 E] (b : hilbert_basis ι 𝕜 E) :
@[protected]
theorem hilbert_basis.has_sum_repr_symm {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [inner_product_space 𝕜 E] (b : hilbert_basis ι 𝕜 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} [inner_product_space 𝕜 E] (b : hilbert_basis ι 𝕜 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} [inner_product_space 𝕜 E] (b : hilbert_basis ι 𝕜 E) :
@[protected]
theorem hilbert_basis.has_sum_inner_mul_inner {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [inner_product_space 𝕜 E] (b : hilbert_basis ι 𝕜 E) (x y : E) :
has_sum (λ (i : ι), has_inner.inner x (b i) * has_inner.inner (b i) y) (has_inner.inner x y)
@[protected]
theorem hilbert_basis.summable_inner_mul_inner {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [inner_product_space 𝕜 E] (b : hilbert_basis ι 𝕜 E) (x y : E) :
summable (λ (i : ι), has_inner.inner x (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} [inner_product_space 𝕜 E] (b : hilbert_basis ι 𝕜 E) (x y : E) :
@[protected]
noncomputable def hilbert_basis.to_orthonormal_basis {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [inner_product_space 𝕜 E] [fintype ι] (b : hilbert_basis ι 𝕜 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} [inner_product_space 𝕜 E] [fintype ι] (b : hilbert_basis ι 𝕜 E) :
@[protected]
theorem hilbert_basis.has_sum_orthogonal_projection {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [inner_product_space 𝕜 E] {U : submodule 𝕜 E} [complete_space U] (b : hilbert_basis ι 𝕜 U) (x : E) :
theorem hilbert_basis.finite_spans_dense {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [inner_product_space 𝕜 E] (b : hilbert_basis ι 𝕜 E) :
@[protected]
noncomputable def hilbert_basis.mk {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [inner_product_space 𝕜 E] [cplt : complete_space E] {v : ι E} (hv : orthonormal 𝕜 v) (hsp : (submodule.span 𝕜 (set.range v)).topological_closure) :
hilbert_basis ι 𝕜 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} [inner_product_space 𝕜 E] [cplt : complete_space E] {v : ι E} (hv : orthonormal 𝕜 v) (h : (submodule.span 𝕜 (set.range v)).topological_closure) (i : ι) :
@[protected, simp]
theorem hilbert_basis.coe_mk {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [inner_product_space 𝕜 E] [cplt : complete_space E] {v : ι E} (hv : orthonormal 𝕜 v) (hsp : (submodule.span 𝕜 (set.range v)).topological_closure) :
@[protected]
noncomputable def hilbert_basis.mk_of_orthogonal_eq_bot {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [inner_product_space 𝕜 E] [cplt : complete_space E] {v : ι E} (hv : orthonormal 𝕜 v) (hsp : (submodule.span 𝕜 (set.range v)) = ) :
hilbert_basis ι 𝕜 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} [inner_product_space 𝕜 E] [cplt : complete_space E] {v : ι E} (hv : orthonormal 𝕜 v) (hsp : (submodule.span 𝕜 (set.range v)) = ) :
@[protected]
noncomputable def orthonormal_basis.to_hilbert_basis {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [inner_product_space 𝕜 E] [cplt : complete_space E] [fintype ι] (b : orthonormal_basis ι 𝕜 E) :
hilbert_basis ι 𝕜 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} [inner_product_space 𝕜 E] [cplt : complete_space E] [fintype ι] (b : orthonormal_basis ι 𝕜 E) :
theorem orthonormal.exists_hilbert_basis_extension {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [inner_product_space 𝕜 E] [cplt : complete_space E] {s : set E} (hs : orthonormal 𝕜 coe) :
(w : set E) (b : hilbert_basis w 𝕜 E), s w b = coe

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) [inner_product_space 𝕜 E] [cplt : complete_space E] :
(w : set E) (b : hilbert_basis w 𝕜 E), b = coe

A Hilbert space admits a Hilbert basis.