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.

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))
@[protected, instance]
noncomputable def lp.inner_product_space {ฮน : Type u_1} {๐•œ : Type u_2} [is_R_or_C ๐•œ] {G : ฮน โ†’ Type u_4} [ฮ  (i : ฮน), inner_product_space ๐•œ (G i)] :
Equations
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) :

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) :
@[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.

noncomputable def orthogonal_family.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 : orthogonal_family ๐•œ V) [โˆ€ (i : ฮน), complete_space (G i)] (hV' : (โจ† (i : ฮน), (V i).to_linear_map.range).topological_closure = โŠค) :

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
@[protected]
theorem orthogonal_family.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 : orthogonal_family ๐•œ V) [โˆ€ (i : ฮน), complete_space (G i)] (hV' : (โจ† (i : ฮน), (V i).to_linear_map.range).topological_closure = โŠค) (w : โ†ฅ(lp G 2)) :
โ‡‘((hV.linear_isometry_equiv hV').symm) w = โˆ‘' (i : ฮน), โ‡‘(V i) (โ‡‘w i)

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.

@[protected]
theorem orthogonal_family.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 : orthogonal_family ๐•œ V) [โˆ€ (i : ฮน), complete_space (G i)] (hV' : (โจ† (i : ฮน), (V i).to_linear_map.range).topological_closure = โŠค) (w : โ†ฅ(lp G 2)) :
has_sum (ฮป (i : ฮน), โ‡‘(V i) (โ‡‘w i)) (โ‡‘((hV.linear_isometry_equiv hV').symm) w)

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.

@[protected, simp]
theorem orthogonal_family.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 : orthogonal_family ๐•œ V) [โˆ€ (i : ฮน), complete_space (G i)] (hV' : (โจ† (i : ฮน), (V i).to_linear_map.range).topological_closure = โŠค) {i : ฮน} (x : G i) :

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.

@[protected, simp]
theorem orthogonal_family.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 : orthogonal_family ๐•œ V) [โˆ€ (i : ฮน), complete_space (G i)] (hV' : (โจ† (i : ฮน), (V i).to_linear_map.range).topological_closure = โŠค) (Wโ‚€ : ฮ โ‚€ (i : ฮน), G i) :
โ‡‘((hV.linear_isometry_equiv hV').symm) (Wโ‚€.sum (lp.single 2)) = Wโ‚€.sum (ฮป (i : ฮน), โ‡‘(V i))

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.

@[protected, simp]
theorem orthogonal_family.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 : orthogonal_family ๐•œ V) [โˆ€ (i : ฮน), complete_space (G i)] (hV' : (โจ† (i : ฮน), (V i).to_linear_map.range).topological_closure = โŠค) (Wโ‚€ : ฮ โ‚€ (i : ฮน), G i) :
โ‡‘(โ‡‘(hV.linear_isometry_equiv hV') (Wโ‚€.sum (ฮป (i : ฮน), โ‡‘(V i)))) = โ‡‘Wโ‚€

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 #

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 : ฮน) :
@[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 : ฮน) :
@[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 : ฮน) :
@[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) :
orthonormal ๐•œ โ‡‘b
@[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]
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
@[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))แ—ฎ = โŠฅ) :
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.