OAI/Analysis/KadisonKastler/CommonRankCoordinates.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Fixed-rank coordinates for a represented common C-star source

The common spectral model and its Borel representations give a unitary on each fixed-rank stratum.

  1. structure OAI.KadisonKastler.BorelCommonModel line 31
  2. def OAI.KadisonKastler.borelCommonModel line 39
  3. def OAI.KadisonKastler.commonRankBasis line 44
  4. theorem OAI.KadisonKastler.commonRankBasis_total line 48
  5. def OAI.KadisonKastler.commonModelProjection line 59
  6. theorem OAI.KadisonKastler.commonModelProjection_idempotent line 62
  7. theorem OAI.KadisonKastler.commonModelProjection_norm_le line 67
  8. theorem OAI.KadisonKastler.commonModelProjection_measurable line 72
  9. theorem OAI.KadisonKastler.commonModelProjection_action line 76
  10. def OAI.KadisonKastler.commonRankCoordinates line 82
  11. theorem OAI.KadisonKastler.commonRankCoordinates_action line 91