OAI/Analysis/KadisonKastler/CornerLossBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Cost of removing a subprojection from a symmetric corner

For a conjugation-fixed vector, removing p from q costs at most twice its left p-mass inside the old two-sided corner.

  1. theorem OAI.KadisonKastler.two_projection_union_norm_sq_le line 20
  2. theorem OAI.KadisonKastler.modularQuadratic_projection_fixed line 42
  3. theorem OAI.KadisonKastler.cornerProjection_loss_bound line 52
  4. theorem OAI.KadisonKastler.cornerProjection_residual_bound line 80