# Documentation

Mathlib.Analysis.InnerProductSpace.l2Space

# Hilbert sum of a family of inner product spaces #

Given a family (G : ι → Type*) [Π i, InnerProductSpace 𝕜 (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 IsHilbertSum 𝕜 G V, where V : Π i, G i →ₗᵢ[𝕜] E, expressing that V is an OrthogonalFamily and that the associated map lp G 2 →ₗᵢ[𝕜] E is surjective.

## Main definitions #

• OrthogonalFamily.linearIsometry: 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.

• IsHilbertSum: 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, IsHilbertSum 𝕜 G V means that V is an OrthogonalFamily and that the above linear isometry is surjective.

• IsHilbertSum.linearIsometryEquiv: 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 OrthogonalFamily.linearIsometry can be upgraded to a LinearIsometryEquiv.

• HilbertBasis: We define a Hilbert basis of a Hilbert space E to be a structure whose single field HilbertBasis.repr is an isometric isomorphism of E with ℓ²(ι, 𝕜) (i.e., the Hilbert sum of ι copies of 𝕜). This parallels the definition of Basis, in LinearAlgebra.Basis, as an isomorphism of an R-module with ι →₀ R.

• HilbertBasis.instCoeFun: 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.coeFun in LinearAlgebra.Basis.

• HilbertBasis.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 LinearAlgebra.Basis.

• HilbertBasis.mkOfOrthogonalEqBot: 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.instInnerProductSpace: Construction of the inner product space instance on the Hilbert sum lp G 2. Note that from the file Analysis.NormedSpace.lpSpace, the space lp G 2 already held a normed space instance (lp.normedSpace), and if each G i is a Hilbert space (i.e., complete), then lp G 2 was already known to be complete (lp.completeSpace). So the work here is to define the inner product and show it is compatible.

• OrthogonalFamily.range_linearIsometry: 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 OrthogonalFamily.linearIsometry of the Hilbert sum of G into E is the closure of the span of the images of the G i.

• HilbertBasis.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⟫.

• HilbertBasis.hasSum_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_hilbertBasis: A Hilbert space admits a Hilbert basis.

## Keywords #

Hilbert space, Hilbert sum, l2, Hilbert basis, unitary equivalence, isometric isomorphism

ℓ²(ι, 𝕜) is the Hilbert space of square-summable functions ι → 𝕜, herein implemented as lp (fun i : ι => 𝕜) 2.

Instances For

### Inner product space structure on lp G 2#

theorem lp.summable_inner {ι : Type u_1} {𝕜 : Type u_2} [] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] (f : { x // x lp G 2 }) (g : { x // x lp G 2 }) :
Summable fun i => inner (f i) (g i)
instance lp.instInnerProductSpace {ι : Type u_1} {𝕜 : Type u_2} [] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] :
InnerProductSpace 𝕜 { x // x lp G 2 }
theorem lp.inner_eq_tsum {ι : Type u_1} {𝕜 : Type u_2} [] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] (f : { x // x lp G 2 }) (g : { x // x lp G 2 }) :
inner f g = ∑' (i : ι), inner (f i) (g i)
theorem lp.hasSum_inner {ι : Type u_1} {𝕜 : Type u_2} [] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] (f : { x // x lp G 2 }) (g : { x // x lp G 2 }) :
HasSum (fun i => inner (f i) (g i)) (inner f g)
theorem lp.inner_single_left {ι : Type u_1} {𝕜 : Type u_2} [] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] (i : ι) (a : G i) (f : { x // x lp G 2 }) :
inner (lp.single 2 i a) f = inner a (f i)
theorem lp.inner_single_right {ι : Type u_1} {𝕜 : Type u_2} [] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] (i : ι) (a : G i) (f : { x // x lp G 2 }) :
inner f (lp.single 2 i a) = inner (f i) a

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

theorem OrthogonalFamily.summable_of_lp {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] [cplt : ] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : ) (f : { x // x lp G 2 }) :
Summable fun i => ↑(V i) (f i)
def OrthogonalFamily.linearIsometry {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] [cplt : ] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : ) :
{ x // x lp G 2 } →ₗᵢ[𝕜] E

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

Instances For
theorem OrthogonalFamily.linearIsometry_apply {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] [cplt : ] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : ) (f : { x // x lp G 2 }) :
= ∑' (i : ι), ↑(V i) (f i)
theorem OrthogonalFamily.hasSum_linearIsometry {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] [cplt : ] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : ) (f : { x // x lp G 2 }) :
HasSum (fun i => ↑(V i) (f i)) ()
@[simp]
theorem OrthogonalFamily.linearIsometry_apply_single {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] [cplt : ] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : ) {i : ι} (x : G i) :
↑() (lp.single 2 i x) = ↑(V i) x
@[simp]
theorem OrthogonalFamily.linearIsometry_apply_dfinsupp_sum_single {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] [cplt : ] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : ) (W₀ : Π₀ (i : ι), G i) :
↑() (DFinsupp.sum W₀ ()) = DFinsupp.sum W₀ fun i => ↑(V i)
theorem OrthogonalFamily.range_linearIsometry {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] [cplt : ] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : ) [∀ (i : ι), CompleteSpace (G i)] :
LinearMap.range ().toLinearMap = Submodule.topologicalClosure (⨆ (i : ι), LinearMap.range (V i).toLinearMap)

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 IsHilbertSum {ι : Type u_1} (𝕜 : Type u_2) [] {E : Type u_3} [] [cplt : ] (G : ιType u_4) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] (V : (i : ι) → G i →ₗᵢ[𝕜] E) :
• ofSurjective :: (
• OrthogonalFamily :

The orthogonal family constituting the summands in the Hilbert sum.

• surjective_isometry :

The isometry lp G 2 → E induced by the orthogonal family is surjective.

• )

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

Instances For
theorem IsHilbertSum.mk {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] [cplt : ] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} [∀ (i : ι), CompleteSpace (G i)] (hVortho : ) (hVtotal : Submodule.topologicalClosure (⨆ (i : ι), LinearMap.range (V i).toLinearMap)) :
IsHilbertSum 𝕜 G 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 IsHilbertSum.mkInternal {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] [cplt : ] (F : ι) [∀ (i : ι), CompleteSpace { x // x F i }] (hFortho : OrthogonalFamily 𝕜 (fun i => { x // x F i }) fun i => Submodule.subtypeₗᵢ (F i)) (hFtotal : Submodule.topologicalClosure (⨆ (i : ι), F i)) :
IsHilbertSum 𝕜 (fun i => { x // x F i }) fun i => Submodule.subtypeₗᵢ (F i)

This is Orthonormal.isHilbertSum in the case of actual inclusions from subspaces.

noncomputable def IsHilbertSum.linearIsometryEquiv {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] [cplt : ] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : IsHilbertSum 𝕜 G V) :
E ≃ₗᵢ[𝕜] { x // x 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 OrthogonalFamily.linearIsometry.

Instances For
theorem IsHilbertSum.linearIsometryEquiv_symm_apply {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] [cplt : ] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : IsHilbertSum 𝕜 G V) (w : { x // x lp G 2 }) :
= ∑' (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.

theorem IsHilbertSum.hasSum_linearIsometryEquiv_symm {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] [cplt : ] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : IsHilbertSum 𝕜 G V) (w : { x // x lp G 2 }) :
HasSum (fun 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, and this sum indeed converges.

@[simp]
theorem IsHilbertSum.linearIsometryEquiv_symm_apply_single {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] [cplt : ] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : IsHilbertSum 𝕜 G V) {i : ι} (x : G i) :
↑() (lp.single 2 i x) = ↑(V i) x

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.

@[simp]
theorem IsHilbertSum.linearIsometryEquiv_symm_apply_dfinsupp_sum_single {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] [cplt : ] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : IsHilbertSum 𝕜 G V) (W₀ : Π₀ (i : ι), G i) :
↑() (DFinsupp.sum W₀ ()) = DFinsupp.sum W₀ fun 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.

@[simp]
theorem IsHilbertSum.linearIsometryEquiv_apply_dfinsupp_sum_single {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] [cplt : ] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : IsHilbertSum 𝕜 G V) (W₀ : Π₀ (i : ι), G i) :
↑(↑() (DFinsupp.sum W₀ fun 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.isHilbertSum {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] [cplt : ] {v : ιE} (hv : ) (hsp : ) :
IsHilbertSum 𝕜 (fun x => 𝕜) fun i => LinearIsometry.toSpanSingleton 𝕜 E (_ : v i = 1)

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

theorem Submodule.isHilbertSumOrthogonal {𝕜 : Type u_2} [] {E : Type u_3} [] [cplt : ] (K : ) [hK : CompleteSpace { x // x K }] :
IsHilbertSum 𝕜 (fun b => { x // x bif b then K else K }) fun b => Submodule.subtypeₗᵢ (bif b then K else K)

### Hilbert bases #

structure HilbertBasis (ι : Type u_1) (𝕜 : Type u_2) [] (E : Type u_3) [] :
Type (max (max u_1 u_2) u_3)
• ofRepr :: (
• repr : E ≃ₗᵢ[𝕜] { x // x lp (fun i => 𝕜) 2 }

The linear isometric equivalence implementing identifying the Hilbert space with ℓ².

• )

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

Instances For
instance HilbertBasis.instCoeFun {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] :
CoeFun (HilbertBasis ι 𝕜 E) fun x => ιE

b i is the ith basis vector.

@[simp]
theorem HilbertBasis.repr_symm_single {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] (b : HilbertBasis ι 𝕜 E) (i : ι) :
↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1) = (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i
theorem HilbertBasis.repr_self {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] (b : HilbertBasis ι 𝕜 E) (i : ι) :
b.repr ((fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) = lp.single 2 i 1
theorem HilbertBasis.repr_apply_apply {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] (b : HilbertBasis ι 𝕜 E) (v : E) (i : ι) :
↑(b.repr v) i = inner ((fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) v
@[simp]
theorem HilbertBasis.orthonormal {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] (b : HilbertBasis ι 𝕜 E) :
Orthonormal 𝕜 fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)
theorem HilbertBasis.hasSum_repr_symm {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] (b : HilbertBasis ι 𝕜 E) (f : { x // x lp (fun i => 𝕜) 2 }) :
HasSum (fun i => f i (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) (↑(LinearIsometryEquiv.symm b.repr) f)
theorem HilbertBasis.hasSum_repr {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] (b : HilbertBasis ι 𝕜 E) (x : E) :
HasSum (fun i => ↑(b.repr x) i (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) x
@[simp]
theorem HilbertBasis.dense_span {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] (b : HilbertBasis ι 𝕜 E) :
theorem HilbertBasis.hasSum_inner_mul_inner {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] (b : HilbertBasis ι 𝕜 E) (x : E) (y : E) :
HasSum (fun i => inner x ((fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) * inner ((fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) y) (inner x y)
theorem HilbertBasis.summable_inner_mul_inner {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] (b : HilbertBasis ι 𝕜 E) (x : E) (y : E) :
Summable fun i => inner x ((fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) * inner ((fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) y
theorem HilbertBasis.tsum_inner_mul_inner {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] (b : HilbertBasis ι 𝕜 E) (x : E) (y : E) :
∑' (i : ι), inner x ((fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) * inner ((fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) y = inner x y
def HilbertBasis.toOrthonormalBasis {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] [] (b : HilbertBasis ι 𝕜 E) :

A finite Hilbert basis is an orthonormal basis.

Instances For
@[simp]
theorem HilbertBasis.coe_toOrthonormalBasis {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] [] (b : HilbertBasis ι 𝕜 E) :
= fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)
theorem HilbertBasis.hasSum_orthogonalProjection {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] {U : } [CompleteSpace { x // x U }] (b : HilbertBasis ι 𝕜 { x // x U }) (x : E) :
HasSum (fun i => inner (↑((fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i)) x (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) (↑() x)
theorem HilbertBasis.finite_spans_dense {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] (b : HilbertBasis ι 𝕜 E) :
Submodule.topologicalClosure (⨆ (J : ), Submodule.span 𝕜 ↑(Finset.image (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) J)) =
def HilbertBasis.mk {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] [cplt : ] {v : ιE} (hv : ) (hsp : ) :
HilbertBasis ι 𝕜 E

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

Instances For
theorem Orthonormal.linearIsometryEquiv_symm_apply_single_one {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] [cplt : ] {v : ιE} (hv : ) (h : ) (i : ι) :
↑(LinearIsometryEquiv.symm (IsHilbertSum.linearIsometryEquiv (_ : IsHilbertSum 𝕜 (fun x => 𝕜) fun i => LinearIsometry.toSpanSingleton 𝕜 E (_ : v i = 1)))) (lp.single 2 i 1) = v i
@[simp]
theorem HilbertBasis.coe_mk {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] [cplt : ] {v : ιE} (hv : ) (hsp : ) :
(fun i => ↑(LinearIsometryEquiv.symm (HilbertBasis.mk hv hsp).repr) (lp.single 2 i 1)) = v
def HilbertBasis.mkOfOrthogonalEqBot {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] [cplt : ] {v : ιE} (hv : ) (hsp : () = ) :
HilbertBasis ι 𝕜 E

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

Instances For
@[simp]
theorem HilbertBasis.coe_mkOfOrthogonalEqBot {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] [cplt : ] {v : ιE} (hv : ) (hsp : () = ) :
(fun i => ↑(LinearIsometryEquiv.symm ().repr) (lp.single 2 i 1)) = v
def OrthonormalBasis.toHilbertBasis {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] [cplt : ] [] (b : ) :
HilbertBasis ι 𝕜 E

An orthonormal basis is a Hilbert basis.

Instances For
@[simp]
theorem OrthonormalBasis.coe_toHilbertBasis {ι : Type u_1} {𝕜 : Type u_2} [] {E : Type u_3} [] [cplt : ] [] (b : ) :
(fun i => ↑() (lp.single 2 i 1)) = b
theorem Orthonormal.exists_hilbertBasis_extension {𝕜 : Type u_2} [] {E : Type u_3} [] [cplt : ] {s : Set E} (hs : Orthonormal 𝕜 Subtype.val) :
w b, s w (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) = Subtype.val

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

theorem exists_hilbertBasis (𝕜 : Type u_2) [] (E : Type u_3) [] [cplt : ] :
w b, (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) = Subtype.val

A Hilbert space admits a Hilbert basis.