OAI/Analysis/KadisonKastler/ProjectionNormDecomposition.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Squared-norm decompositions for nested projections

  1. theorem OAI.KadisonKastler.projection_apply_norm_le line 16
  2. theorem OAI.KadisonKastler.projection_complement_inner line 20
  3. theorem OAI.KadisonKastler.projection_norm_sq_decomposition line 30
  4. theorem OAI.KadisonKastler.nested_projection_reverse line 40
  5. theorem OAI.KadisonKastler.nested_projection_norm_sq_eq line 46
  6. theorem OAI.KadisonKastler.nested_projection_norm_sq line 63