OAI/Analysis/BoundedHochschild/ProjectionDefectRigidity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

In the minimal averaging family, an algebra-valued projection defect must vanish: a nonzero defect would give a positive spectral gap contradicting the projection-compression norm identity.

  1. theorem OAI.BoundedHochschild.KadisonRingrose.projection_defect_eq_zero line 22