OAI/Analysis/Commutator/FreePropagation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.zeroLimitSpace line 20
2. lemma OAI.Kadison.zeroLimitSpace_closed line 32
3. lemma OAI.Kadison.FreeCreation.tailProjection_mul_tail line 58
4. lemma OAI.Kadison.FreeCreation.tailProjection_mul_centered_tail line 77
5. lemma OAI.Kadison.FreeCreation.norm_tailProjection_mul line 83
6. lemma OAI.Kadison.FreeCreation.wordVector_mem_tail line 101
7. lemma OAI.Kadison.FreeCreation.tailProjection_mul_word line 107
8. theorem OAI.Kadison.FreeCreation.tailProjection_mul_tendsto_zero line 138
9. lemma OAI.Kadison.FreeCreation.mul_head_norm line 212
10. lemma OAI.Kadison.FreeCreation.repeated_prefix_head line 222
11. lemma OAI.Kadison.FreeCreation.prefix_split_bound line 241
12. theorem OAI.Kadison.FreeCreation.repeated_prefix_eventual_bound line 267
13. lemma OAI.Kadison.FreeCreation.norm_mul_supported line 303
14. lemma OAI.Kadison.propagation_limit_bound line 326