OAI/Analysis/KadisonKastler/ProjectionCommutatorEnergy.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The energy removed by a two-sided projection cut

For commuting left and right projections, the diagonal cut is an orthogonal projection. Its discarded squared norm is exactly the squared norm of their difference acting on the vector.

  1. def OAI.KadisonKastler.pairedProjectionCut line 18
  2. theorem OAI.KadisonKastler.pairedProjectionCut_isProjection line 21
  3. theorem OAI.KadisonKastler.pairedProjectionCut_complement line 33
  4. theorem OAI.KadisonKastler.pairedProjectionCut_discarded_norm line 40
  5. theorem OAI.KadisonKastler.pairedProjectionCut_energy line 59