Theorems · Inductive type · functional analysis

IsHilbertSum

{ι : Type u_1} →
  (𝕜 : Type u_2) →
    [inst : RCLike 𝕜] →
      {E : Type u_3} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            (G : ι → Type u_4) →
              [inst_3 : (i : ι) → NormedAddCommGroup (G i)] →
                [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] → [CompleteSpace E] → ((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 DirectSum.IsInternal, except that we don't express it in terms of actual submodules.

Defined in

Mathlib.Analysis.InnerProductSpace.l2Space

Cited by

12 results in Mathlib

Foundations

Depth 46 from the axioms · uses propext, Quot.sound

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceNormedAddCommGroupInnerProductSpaceCompleteSpace