OAI/Analysis/KadisonKastler/CenteredVectorApproximation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Centered cyclic approximation and commutator defects

  1. theorem OAI.KadisonKastler.exists_centered_algebra_vector_near_of_mem_closure line 16
  2. theorem OAI.KadisonKastler.exists_centered_algebra_vector_near line 48
  3. theorem OAI.KadisonKastler.centralVectorDefect_on_algebra_vector line 54
  4. theorem OAI.KadisonKastler.commutator_vector_norm_le_central_defects line 72
  5. theorem OAI.KadisonKastler.centralVectorDefect_vector_lipschitz line 84