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

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) :
is_hilbert_sum ๐•œ E 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} [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) :

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 : ฮน) :
@[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]
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) :
โˆ‘' (i : ฮน), has_inner.inner x (โ‡‘b i) * has_inner.inner (โ‡‘b i) y = has_inner.inner x y
@[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) :
orthonormal_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.