OAI/Analysis/KadisonSimilarity/Representation/DyadicCornerHom.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The finite dyadic spectral sums form contractive unital star homomorphisms into the original corner.

  1. theorem OAI.KadisonSimilarity.dyadicProjection_le_root line 23
  2. theorem OAI.KadisonSimilarity.dyadicEval_supported line 29
  3. def OAI.KadisonSimilarity.dyadicCornerHom line 41
  4. theorem OAI.KadisonSimilarity.dyadicCornerHom_coe line 68
  5. theorem OAI.KadisonSimilarity.norm_dyadicCornerHom_le line 73
  6. theorem OAI.KadisonSimilarity.dyadicCornerHom_refine line 79