OAI/Analysis/Commutator/HilbertSequence.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Kadison.HilbertSequence.Pre line 20
2. def OAI.Kadison.HilbertSequence.equiv line 23
3. instance OAI.Kadison.HilbertSequence.(instance at line 29) line 29
4. instance OAI.Kadison.HilbertSequence.(instance at line 31) line 31
5. lemma OAI.Kadison.HilbertSequence.seq_add line 34
6. lemma OAI.Kadison.HilbertSequence.seq_smul line 36
7. lemma OAI.Kadison.HilbertSequence.seq_zero line 39
8. lemma OAI.Kadison.HilbertSequence.inner_bounded line 41
9. def OAI.Kadison.HilbertSequence.form line 47
10. lemma OAI.Kadison.HilbertSequence.tendsto_form line 50
11. instance OAI.Kadison.HilbertSequence.core line 54
12. instance OAI.Kadison.HilbertSequence.(instance at line 69) line 69
13. instance OAI.Kadison.HilbertSequence.(instance at line 72) line 72
14. lemma OAI.Kadison.HilbertSequence.pre_inner line 74
15. lemma OAI.Kadison.HilbertSequence.tendsto_inner line 76
16. lemma OAI.Kadison.HilbertSequence.tendsto_norm line 80
17. abbrev OAI.Kadison.HilbertSequence.Space line 85
18. lemma OAI.Kadison.HilbertSequence.norm_coe_tendsto line 87
19. lemma OAI.Kadison.HilbertSequence.coe_eq_zero_iff line 92
20. def OAI.Kadison.HilbertSequence.constantPre line 101
21. lemma OAI.Kadison.HilbertSequence.norm_constantPre line 103
22. def OAI.Kadison.HilbertSequence.constantPreMap line 106
23. def OAI.Kadison.HilbertSequence.constant line 122
24. lemma OAI.Kadison.HilbertSequence.constant_apply line 125