OAI/Analysis/OInfinity/VacuumCorner.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Finite Fock coefficients from an unused Cuntz generator

For words in the first N generators, the next generator has exactly the vacuum annihilation relations. This realizes every finite Fock compression of such a word as a corner in the Cuntz algebra itself.

  1. def OAI.WeakPureInfiniteness.oInfinityVacuumWord line 24
  2. lemma OAI.WeakPureInfiniteness.oInfinityVacuumWord_relations line 28
  3. def OAI.WeakPureInfiniteness.finiteAlphabetWord line 60
  4. lemma OAI.WeakPureInfiniteness.finiteAlphabetWord_nil line 63
  5. lemma OAI.WeakPureInfiniteness.finiteAlphabetWord_cons line 65
  6. def OAI.WeakPureInfiniteness.finiteAlphabetPop line 70
  7. def OAI.WeakPureInfiniteness.finiteAlphabetRun line 74
  8. def OAI.WeakPureInfiniteness.vacuumRunValue line 79
  9. lemma OAI.WeakPureInfiniteness.oInfinityVacuumWord_annihilate line 82
  10. lemma OAI.WeakPureInfiniteness.finiteAlphabetWord_vacuum_action line 97
  11. def OAI.WeakPureInfiniteness.finiteAlphabetBasis line 123
  12. def OAI.WeakPureInfiniteness.fockRunValue line 126
  13. lemma OAI.WeakPureInfiniteness.finiteAlphabetBasis_create line 129
  14. lemma OAI.WeakPureInfiniteness.finiteAlphabetBasis_annihilate line 133
  15. lemma OAI.WeakPureInfiniteness.finiteAlphabetWord_fock_action line 146
  16. lemma OAI.WeakPureInfiniteness.finiteAlphabetBasis_inner line 176
  17. lemma OAI.WeakPureInfiniteness.finiteAlphabetWord_coefficient line 182
  18. lemma OAI.WeakPureInfiniteness.oInfinityVacuumWord_ofFn line 196
  19. def OAI.WeakPureInfiniteness.finiteVacuumCorner line 207
  20. lemma OAI.WeakPureInfiniteness.finiteVacuumCorner_relations line 210
  21. lemma OAI.WeakPureInfiniteness.finiteVacuumCorner_compression line 225
  22. lemma OAI.WeakPureInfiniteness.exists_finiteAlphabet_lift line 236
  23. lemma OAI.WeakPureInfiniteness.finiteVacuumCorner_cuntzWord line 246
  24. lemma OAI.WeakPureInfiniteness.finiteVacuumCorner_polynomial line 253
  25. lemma OAI.WeakPureInfiniteness.exists_polynomial_alphabet_bound line 268