OAI/Analysis/KadisonKastler/PositiveFactorCorners.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Positive norms in faithful factor corners

  1. theorem OAI.KadisonKastler.cornerCompression_nonneg line 17
  2. theorem OAI.KadisonKastler.cornerCompression_mono line 25
  3. theorem OAI.KadisonKastler.norm_cornerCompression_of_factor line 31
  4. theorem OAI.KadisonKastler.norm_add_nonneg_scalar line 39
  5. theorem OAI.KadisonKastler.nontrivial_projection_range line 53
  6. theorem OAI.KadisonKastler.norm_add_scalar_le_of_order line 64
  7. theorem OAI.KadisonKastler.norm_add_le_of_compressed_lower line 73