OAI/Analysis/KadisonKastler/RegularCoreBasis.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A countable scalar basis for the real regular space

Disjoint unit intervals supply an infinite orthonormal set. A maximal orthonormal extension is countable by separability, hence can be indexed by the natural numbers. No representation-theoretic input is used.

  1. def OAI.KadisonKastler.regularIntervalVector line 22
  2. theorem OAI.KadisonKastler.regularIntervalVector_orthonormal line 26
  3. theorem OAI.KadisonKastler.orthonormal_countable line 41
  4. theorem OAI.KadisonKastler.exists_regularScalarBasis line 61

    Source documentation

    The scalar real-line L² space has an actual natural-number Hilbert basis.

    theorem exists_regularScalarBasis :
    Nonempty (HilbertBasis ℕ ℂ (Lp ℂ 2 (volume : Measure ℝ))) := by
…
  5. def OAI.KadisonKastler.regularScalarBasis line 87

    Source documentation

    One fixed scalar basis; its only role is to select Hilbert coordinates.

    def regularScalarBasis : HilbertBasis ℕ ℂ (Lp ℂ 2 (volume : Measure ℝ)) :=
…