OAI/Analysis/KadisonKastler/PartialPinchingRefinement.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Adding one cut to a partial pinching

Already selected orthogonal corners are left fixed. Refining the remaining corner increases the residual squared norm by exactly the local commutator energy. This is the additive identity used by the maximal-family argument.

  1. theorem OAI.KadisonKastler.orthogonal_projection_mul_reverse line 21
  2. theorem OAI.KadisonKastler.orthogonal_sum_nested line 26
  3. theorem OAI.KadisonKastler.nested_projection_residual_energy line 36
  4. theorem OAI.KadisonKastler.partialPinching_refinement_isProjection line 52
  5. theorem OAI.KadisonKastler.partialPinching_refinement_energy line 65