OAI/Analysis/KadisonKastler/BicentralizerProjection.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

A contractive state-preserving projection onto the bicentralizer

The compact asymptotic orbit hull supplies an element of the bicentralizer. Its pairings with every bicentralizer vector are prescribed, which makes the choice unique and proves linearity. The orbit norm bound gives the contractive projection on the original algebra.

  1. theorem OAI.KadisonKastler.exists_bicentralizer_orbit_point line 23
  2. def OAI.KadisonKastler.bicentralizerProjection line 30
  3. theorem OAI.KadisonKastler.bicentralizerProjection_mem line 34
  4. theorem OAI.KadisonKastler.bicentralizerProjection_orbit line 39
  5. theorem OAI.KadisonKastler.bicentralizerProjection_pairing line 44
  6. theorem OAI.KadisonKastler.eq_of_bicentralizer_pairings line 51
  7. theorem OAI.KadisonKastler.bicentralizerProjection_add line 68
  8. theorem OAI.KadisonKastler.bicentralizerProjection_smul line 83
  9. theorem OAI.KadisonKastler.bicentralizerProjection_norm_le line 94
  10. def OAI.KadisonKastler.bicentralizerProjectionCLM line 99
  11. theorem OAI.KadisonKastler.bicentralizerProjection_fixed line 110
  12. theorem OAI.KadisonKastler.bicentralizerProjection_idempotent line 116
  13. theorem OAI.KadisonKastler.bicentralizerProjection_state line 122