OAI/Analysis/KadisonKastler/ProjectionRangeFrame.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Hilbert coordinates from measurable projection frames

The nonzero Gram-Schmidt vectors form a Hilbert basis of the actual range. Their ascending enumeration is measurable before restricting to a rank stratum.

  1. theorem OAI.KadisonKastler.frame_mem_range line 22
  2. def OAI.KadisonKastler.projectionRangeFrame line 29

    Source documentation

    The nonzero projected frame, as vectors of the genuine closed range.

    def projectionRangeFrame (P : H →L[ℂ] H) (hP : IsIdempotentElem P)
    (b : ℕ → H) (hb : (Submodule.span ℂ (Set.range b)).topologicalClosure = ⊤)
    (i : {n // gramSchmidtNormed ℂ (fun j => P (b j)) n ≠ 0}) : P.range :=
…
  3. theorem OAI.KadisonKastler.projectionRangeFrame_orthonormal line 35
  4. theorem OAI.KadisonKastler.projectionRangeFrame_orthogonal_eq_bot line 42
  5. def OAI.KadisonKastler.projectionRangeHilbertBasis line 75

    Source documentation

    Every closed projection range has the basis given by its surviving frame.

    def projectionRangeHilbertBasis (P : H →L[ℂ] H) (hP : IsIdempotentElem P)
    (b : ℕ → H) (hb : (Submodule.span ℂ (Set.range b)).topologicalClosure = ⊤) :
    HilbertBasis {n // gramSchmidtNormed ℂ (fun j => P (b j)) n ≠ 0} ℂ P.range := by
…
  6. theorem OAI.KadisonKastler.projectionRangeHilbertBasis_apply line 83
  7. def OAI.KadisonKastler.enumeratedProjectionFrame line 94

    Source documentation

    Ascending enumeration of the nonzero projected frame, with a harmless library default outside its genuine index range.

    def enumeratedProjectionFrame (P : X → H →L[ℂ] H) (b : ℕ → H) (x : X) (k : ℕ) : H :=
…
  8. theorem OAI.KadisonKastler.measurable_enumeratedSequence line 98
  9. theorem OAI.KadisonKastler.enumeratedProjectionFrame_measurable line 110