OAI/Analysis/KadisonKastler/CornerProjectionRefinement.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Energy gained by refining one two-sided corner

Splitting q into p and q-p removes exactly the p-commutator energy inside qJq. These identities are the local step in Haagerup's projection-family amplification argument.

  1. def OAI.KadisonKastler.refinedCornerProjection line 21
  2. theorem OAI.KadisonKastler.modularQuadratic_projection line 28
  3. theorem OAI.KadisonKastler.pairedProjectionCut_eq_quadratics line 37
  4. theorem OAI.KadisonKastler.refinedCornerProjection_mul_left line 44
  5. theorem OAI.KadisonKastler.refinedCornerProjection_mul_right line 53
  6. theorem OAI.KadisonKastler.refinedCornerProjection_isProjection line 62
  7. theorem OAI.KadisonKastler.refinedCornerProjection_nested line 77
  8. theorem OAI.KadisonKastler.refinedCornerProjection_discarded_norm line 83
  9. theorem OAI.KadisonKastler.refinedCornerProjection_energy line 97