OAI/Analysis/Commutator/FreeWordDecomposition.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.FreeWordTensor.boundedLetter line 31
2. lemma OAI.Kadison.FreeWordTensor.asLetter_boundedLetter line 35
3. def OAI.Kadison.FreeWordTensor.paramsOfLetters line 38
4. lemma OAI.Kadison.FreeWordTensor.letters_paramsOfLetters line 43
5. def OAI.Kadison.FreeWordTensor.hilbertWordSpan line 54
6. lemma OAI.Kadison.FreeWordTensor.bounded_word_mem line 57
7. lemma OAI.Kadison.FreeWordTensor.generated_mem_span line 68
8. def OAI.Kadison.FreeWordTensor.generatedOperators line 85
9. lemma OAI.Kadison.FreeWordTensor.total_words_from_generation line 88
10. theorem OAI.Kadison.FreeWordTensor.isHilbertSum_of_generation line 109