OAI/Analysis/KadisonKastler/IsometryComplement.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Complementary projection of an isometric embedding

The formulas below retain the concrete adjoint of the embedding, as needed for a contractive lift with prescribed first coordinate.

  1. def OAI.KadisonKastler.isometryComplement line 22
  2. theorem OAI.KadisonKastler.adjoint_isometry_apply line 25
  3. theorem OAI.KadisonKastler.isometryComplement_adjoint line 29
  4. theorem OAI.KadisonKastler.adjoint_isometry_complement line 33
  5. theorem OAI.KadisonKastler.norm_isometryComplement_sq line 41
  6. theorem OAI.KadisonKastler.isometryComplement_norm_le line 51