OAI/Analysis/CharacterCriterion/MinTensor.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KirchbergRordam.Spatial.map_coe line 43
2. lemma OAI.KirchbergRordam.Spatial.ext line 47
3. lemma OAI.KirchbergRordam.Spatial.map_add_left line 55
4. lemma OAI.KirchbergRordam.Spatial.map_add_right line 61
5. lemma OAI.KirchbergRordam.Spatial.map_smul_left line 67
6. lemma OAI.KirchbergRordam.Spatial.map_smul_right line 73
7. lemma OAI.KirchbergRordam.Spatial.map_mul line 79
8. lemma OAI.KirchbergRordam.Spatial.map_one line 85
9. lemma OAI.KirchbergRordam.Spatial.map_inner_algebraic line 93
10. lemma OAI.KirchbergRordam.Spatial.map_inner line 106
11. lemma OAI.KirchbergRordam.Spatial.map_star line 112
12. lemma OAI.KirchbergRordam.Spatial.left_right_commute line 122
13. lemma OAI.KirchbergRordam.MinTensor.RepresentationPair.commute line 141
14. lemma OAI.KirchbergRordam.MinTensor.bounded line 154
15. lemma OAI.KirchbergRordam.MinTensor.seminorm_apply line 160
16. lemma OAI.KirchbergRordam.MinTensor.le_seminorm line 163
17. lemma OAI.KirchbergRordam.MinTensor.seminorm_le line 169
18. lemma OAI.KirchbergRordam.MinTensor.seminorm_mul_le line 174
19. lemma OAI.KirchbergRordam.MinTensor.seminorm_star line 183
20. lemma OAI.KirchbergRordam.MinTensor.seminorm_cstar line 188
21. lemma OAI.KirchbergRordam.MinTensor.seminorm_tmul_le line 201
22. lemma OAI.KirchbergRordam.MinTensor.seminorm_le_maximal line 203
23. theorem OAI.KirchbergRordam.MinTensor.exists_spatial_crossSeminorm line 207
24. instance OAI.KirchbergRordam.MinTensor.(instance at line 223) line 223
25. def OAI.KirchbergRordam.MinTensor.rawEquiv line 225
26. instance OAI.KirchbergRordam.MinTensor.(instance at line 229) line 229
27. instance OAI.KirchbergRordam.MinTensor.(instance at line 231) line 231
28. lemma OAI.KirchbergRordam.MinTensor.norm_raw line 233
29. instance OAI.KirchbergRordam.MinTensor.(instance at line 236) line 236
30. instance OAI.KirchbergRordam.MinTensor.(instance at line 244) line 244
31. def OAI.KirchbergRordam.MinTensor.of line 246
32. lemma OAI.KirchbergRordam.MinTensor.norm_of line 250
33. lemma OAI.KirchbergRordam.MinTensor.denseRange_of line 252
34. def OAI.KirchbergRordam.MinTensor.includeLeft line 255
35. def OAI.KirchbergRordam.MinTensor.includeRight line 259
36. lemma OAI.KirchbergRordam.MinTensor.legs_commute line 262
37. def OAI.KirchbergRordam.MinTensor.spatialRaw line 271
38. lemma OAI.KirchbergRordam.MinTensor.norm_spatialRaw_le line 276
39. lemma OAI.KirchbergRordam.MinTensor.lipschitz_spatialRaw line 279
40. lemma OAI.KirchbergRordam.MinTensor.continuous_spatialRaw line 284
41. def OAI.KirchbergRordam.MinTensor.extendHom line 286
42. lemma OAI.KirchbergRordam.MinTensor.extendHom_of line 307
43. def OAI.KirchbergRordam.MinTensor.spatialLift line 312
44. def OAI.KirchbergRordam.MinTensor.fromMaximal line 319
45. lemma OAI.KirchbergRordam.MinTensor.fromMaximal_of line 321
46. lemma OAI.KirchbergRordam.MinTensor.fromMaximal_denseRange line 334
47. instance OAI.KirchbergRordam.Spatial.(instance at line 344) line 344
48. instance OAI.KirchbergRordam.MinTensor.(instance at line 353) line 353
49. theorem OAI.KirchbergRordam.States.exists_norming_state line 374