OAI/Analysis/KadisonKastler/RelativeMatrixCone.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Finite-matrix coefficients on the relative standard space

The central-vector projection retains the normalized matrix trace on matrix entries. The conjugate relative action preserves this same space.

  1. theorem OAI.KadisonKastler.amplify_matrix_entry line 24
  2. theorem OAI.KadisonKastler.centralProjection_matrix_entry line 38
  3. theorem OAI.KadisonKastler.relative_conjugate_preserves_central line 62
  4. theorem OAI.KadisonKastler.centralProjection_mixed_coefficient line 71
  5. theorem OAI.KadisonKastler.conjugationOperator_sum line 122

    Distinct definitions of this name: OAI/Analysis/KadisonKastler/ConjugateMatrixStages.lean:30 (different declaration text). Qualify references as OAI.KadisonKastler.conjugationOperator_sum@path.

  6. theorem OAI.KadisonKastler.modularQuadratic_sum_apply line 128
  7. theorem OAI.KadisonKastler.centralProjection_quadratic_coefficients line 139
  8. theorem OAI.KadisonKastler.centralProjection_mem_relative_positiveCone line 155
  9. theorem OAI.KadisonKastler.modularPositiveCone_mono_algebra line 186
  10. theorem OAI.KadisonKastler.relative_positiveCone_mem_central line 198
  11. theorem OAI.KadisonKastler.mem_relative_positiveCone_iff line 216