OAI/Analysis/MarkovType/Renormed.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MarkovSuperreflexivity.Renormed line 17
2. instance OAI.MarkovSuperreflexivity.Renormed.(instance at line 23) line 23
3. instance OAI.MarkovSuperreflexivity.Renormed.(instance at line 24) line 24
4. def OAI.MarkovSuperreflexivity.Renormed.ofOriginal line 26
5. def OAI.MarkovSuperreflexivity.Renormed.toOriginal line 27
6. theorem OAI.MarkovSuperreflexivity.Renormed.toOriginal_ofOriginal line 29
7. theorem OAI.MarkovSuperreflexivity.Renormed.ofOriginal_toOriginal line 32
8. instance OAI.MarkovSuperreflexivity.Renormed.(instance at line 35) line 35
9. theorem OAI.MarkovSuperreflexivity.Renormed.normCore line 37
10. instance OAI.MarkovSuperreflexivity.Renormed.(instance at line 43) line 43
11. instance OAI.MarkovSuperreflexivity.Renormed.(instance at line 44) line 44
12. theorem OAI.MarkovSuperreflexivity.Renormed.norm_ofOriginal line 46
13. theorem OAI.MarkovSuperreflexivity.Renormed.norm_eq line 48
14. def OAI.MarkovSuperreflexivity.Renormed.linearEquiv line 50
15. def OAI.MarkovSuperreflexivity.Renormed.ofOriginalL line 58
16. def OAI.MarkovSuperreflexivity.Renormed.toOriginalL line 61
17. theorem OAI.MarkovSuperreflexivity.Renormed.ofOriginalL_apply line 70
18. theorem OAI.MarkovSuperreflexivity.Renormed.toOriginalL_apply line 72
19. def OAI.MarkovSuperreflexivity.Renormed.continuousLinearEquiv line 74
20. def OAI.MarkovSuperreflexivity.Renormed.uniformEquiv line 79
21. instance OAI.MarkovSuperreflexivity.Renormed.(instance at line 84) line 84