Theorems · Inductive type · functional analysis

HilbertBasis

Type u_1 →
  (𝕜 : Type u_2) →
    [inst : RCLike 𝕜] →
      (E : Type u_3) → [inst_1 : NormedAddCommGroup E] → [InnerProductSpace 𝕜 E] → Type (max (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 ℓ²(ι, 𝕜).

Defined in

Mathlib.Analysis.InnerProductSpace.l2Space

Cited by

28 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

RCLikeNormedAddCommGroupInnerProductSpace