OAI/Analysis/KadisonKastler/StateCommutatorAlgebra.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Algebraic estimates for state centralizer sequences

The state commutator is linear, respects adjoints in norm, and satisfies an explicit product estimate. These facts support the passage from unitary tests to all bounded sequences.

  1. theorem OAI.KadisonKastler.vectorStateCommutator_apply line 21
  2. theorem OAI.KadisonKastler.vectorStateCommutator_add line 24
  3. theorem OAI.KadisonKastler.vectorStateCommutator_smul line 31
  4. theorem OAI.KadisonKastler.vectorStateCommutator_zero line 37
  5. theorem OAI.KadisonKastler.vectorStateCommutator_one line 42
  6. theorem OAI.KadisonKastler.vectorStateCommutator_sub line 47
  7. theorem OAI.KadisonKastler.vectorFunctional_star line 53
  8. theorem OAI.KadisonKastler.vectorStateCommutator_star_apply line 59
  9. theorem OAI.KadisonKastler.vectorStateCommutator_star_norm line 65
  10. theorem OAI.KadisonKastler.vectorStateCommutator_mul_apply line 75
  11. theorem OAI.KadisonKastler.vectorStateCommutator_mul_norm_le line 81
  12. theorem OAI.KadisonKastler.vectorStateCommutator_operator_norm_le line 95