Theorems · Definition · functional analysis

OrthogonalFamily

(𝕜 : Type u_1) →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] →
          {ι : Type u_4} →
            (G : ι → Type u_5) →
              [inst_3 : (i : ι) → SeminormedAddCommGroup (G i)] →
                [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] → ((i : ι) → G i →ₗᵢ[𝕜] E) → Prop

An indexed family of mutually-orthogonal subspaces of an inner product space E. The simple way to express this concept would be as a condition on V : ι → Submodule 𝕜 E. We instead implement it as a condition on a family of inner product spaces each equipped with an isometric embedding into E, thus making it a property of morphisms rather than subobjects. The connection to the subobject spelling is shown in orthogonalFamily_iff_pairwise. This definition is less lightweight, but allows for better definitional properties when the inner product space structure on each of the submodules is important -- for example, when considering their Hilbert sum (PiLp V 2). For example, given an orthonormal set of vectors v : ι → E, we have an associated orthogonal family of one-dimensional subspaces of E, which it is convenient to be able to discuss using ι → 𝕜 rather than Π i : ι, span 𝕜 (v i).

Defined in

Mathlib.Analysis.InnerProductSpace.Subspace

Cited by

48 results in Mathlib

Foundations

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

Assumes

RCLikeSeminormedAddCommGroupInnerProductSpaceSeminormedAddCommGroupInnerProductSpace