OAI/Analysis/KadisonKastler/CornerStatePullback.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Isometric pullback of corner-state comparisons

An isometry onto a projection identifies its corner with the original algebra. The two sandwich maps preserve the norm of corner-supported functionals, so a state comparison on the original factor supplies the same comparison in the corner without a multiplicative loss.

  1. theorem OAI.KadisonKastler.sandwichFunctional_comp line 22
  2. theorem OAI.KadisonKastler.sandwichFunctional_sub line 27
  3. theorem OAI.KadisonKastler.sandwichFunctional_one line 32
  4. theorem OAI.KadisonKastler.sandwichFunctional_projection line 36
  5. theorem OAI.KadisonKastler.sandwichFunctional_norm_le line 41
  6. theorem OAI.KadisonKastler.sandwichFunctional_isometry_norm line 56
  7. theorem OAI.KadisonKastler.sandwichFunctional_supported_pullback_norm line 64
  8. theorem OAI.KadisonKastler.cornerFunctional_idempotent line 72
  9. theorem OAI.KadisonKastler.sandwichFunctional_corner_norm line 81
  10. theorem OAI.KadisonKastler.isometry_norm_le_one line 90
  11. theorem OAI.KadisonKastler.isometry_corner_unitary line 94