OAI/Analysis/KadisonKastler/FactorOffDiagonal.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The spectral-cut step of Paulsen's localized row-averaging argument. If every diagonal compression preserves the norm of a right factor, then every off-diagonal coefficient vanishes and the factored map is right modular.

  1. theorem OAI.KadisonKastler.norm_preserved_by_larger_projection line 29
  2. theorem OAI.KadisonKastler.factor_offDiagonal_eq_zero line 43
  3. theorem OAI.KadisonKastler.right_module_of_no_offDiagonal line 85
  4. theorem OAI.KadisonKastler.right_module_of_factor_diagonal_norm line 104