OAI/Analysis/Commutator/SeparableTestGeometry.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.SeparableTest.generators line 25
  2. def OAI.Kadison.SeparableTest.space line 28
  3. instance OAI.Kadison.SeparableTest.space_complete line 30
  4. instance OAI.Kadison.SeparableTest.space_separable line 33
  5. def OAI.Kadison.SeparableTest.algebra line 36
  6. instance OAI.Kadison.SeparableTest.algebra_closed line 39
  7. instance OAI.Kadison.SeparableTest.algebra_cstar line 42
  8. lemma OAI.Kadison.SeparableTest.entry_mem line 48
  9. def OAI.Kadison.SeparableTest.entries line 51
  10. lemma OAI.Kadison.SeparableTest.algebra_le line 53
  11. lemma OAI.Kadison.SeparableTest.algebra_reduces line 60
  12. lemma OAI.Kadison.SeparableTest.algebra_invariant line 67
  13. lemma OAI.Kadison.SeparableTest.Y_invariant line 70
  14. def OAI.Kadison.SeparableTest.representation line 73
  15. def OAI.Kadison.SeparableTest.restrictedY line 76
  16. def OAI.Kadison.SeparableTest.vector line 78
  17. lemma OAI.Kadison.SeparableTest.include_vector line 81
  18. lemma OAI.Kadison.SeparableTest.vector_norm line 83
  19. lemma OAI.Kadison.SeparableTest.scalar_bound line 86
  20. lemma OAI.Kadison.SeparableTest.seminorm_bound line 94
  21. lemma OAI.Kadison.SeparableTest.matrix_norm_le line 100
  22. lemma OAI.Kadison.SeparableTest.commutator_vector line 105