OAI/Analysis/KadisonSimilarity/FreeProduct/FreeLeadingWords.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Centered leading-word subspaces for the creation operators. Density of all centered words follows by centering the two unrestricted endpoints.

  1. def OAI.KadisonSimilarity.centeredFreeWordVectors line 16
  2. def OAI.KadisonSimilarity.centeredFreeWordSpan line 19
  3. theorem OAI.KadisonSimilarity.centered_word_mem_span line 22
  4. theorem OAI.KadisonSimilarity.full_pairWord_mem_span line 27
  5. theorem OAI.KadisonSimilarity.centeredFreeWordSpan_dense line 68
  6. abbrev OAI.KadisonSimilarity.CenteredWordParameter line 83
  7. abbrev OAI.KadisonSimilarity.LeadingWordParameter line 86
  8. def OAI.KadisonSimilarity.centeredWordFamily line 89
  9. def OAI.KadisonSimilarity.leadingWordFamily line 92
  10. abbrev OAI.KadisonSimilarity.centeredWordSpace line 95
  11. abbrev OAI.KadisonSimilarity.leadingWordSpace line 98
  12. theorem OAI.KadisonSimilarity.inner_leading_opposite_word line 101
  13. theorem OAI.KadisonSimilarity.inner_leading_opposite_space line 108
  14. theorem OAI.KadisonSimilarity.vacuum_mem_centeredWordSpace line 114
  15. theorem OAI.KadisonSimilarity.leadingWordSpace_le_centeredWordSpace line 120
  16. def OAI.KadisonSimilarity.leadingIntoCentered line 126
  17. theorem OAI.KadisonSimilarity.leadingIntoCentered_coe line 131