OAI/Analysis/KadisonSimilarity/Representation/CompressedFieldNorm.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact scalar and matrix norms after restricting actual zero-extension fields to the fibers of the range projection.

  1. theorem OAI.KadisonSimilarity.ae_isometric_field_left_support line 24
  2. theorem OAI.KadisonSimilarity.ae_isometric_field_right_support line 31
  3. theorem OAI.KadisonSimilarity.norm_le_iff_compressed_field line 38
  4. theorem OAI.KadisonSimilarity.matrix_norm_le_iff_compressed_field line 58