OAI/Analysis/CharacterCriterion/HereditaryTransport.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.KirchbergRordam.GenericRW.ConeModel.M2 line 26
2. abbrev OAI.KirchbergRordam.GenericRW.ConeModel.ConeMatrix line 27
3. def OAI.KirchbergRordam.GenericRW.ConeModel.eval line 29
4. def OAI.KirchbergRordam.GenericRW.ConeModel.coneSubalgebra line 39
5. abbrev OAI.KirchbergRordam.GenericRW.ConeModel.Cone line 42
6. def OAI.KirchbergRordam.GenericRW.ConeModel.evaluate line 44
7. lemma OAI.KirchbergRordam.GenericRW.ConeModel.evaluate_sum line 46
8. lemma OAI.KirchbergRordam.GenericRW.ConeModel.evaluate_add line 50
9. lemma OAI.KirchbergRordam.GenericRW.ConeModel.matrixSum_entry line 53
10. instance OAI.KirchbergRordam.GenericRW.ConeModel.(instance at line 56) line 56
11. instance OAI.KirchbergRordam.GenericRW.ConeModel.coneClosed line 59
12. def OAI.KirchbergRordam.GenericRW.ConeModel.coefficients line 64
13. lemma OAI.KirchbergRordam.GenericRW.ConeModel.coefficients_apply line 77
14. lemma OAI.KirchbergRordam.GenericRW.ConeModel.coefficients_zero line 80
15. abbrev OAI.KirchbergRordam.GenericRW.ConeModel.unitCoefficients line 84
16. lemma OAI.KirchbergRordam.GenericRW.ConeModel.unitCoefficients_zero line 87
17. def OAI.KirchbergRordam.GenericRW.ConeModel.toCone line 93
18. lemma OAI.KirchbergRordam.GenericRW.ConeModel.toCone_injective line 99
19. lemma OAI.KirchbergRordam.GenericRW.ConeModel.toCone_surjective line 113
20. def OAI.KirchbergRordam.GenericRW.ConeModel.equiv line 130
21. def OAI.KirchbergRordam.GenericRW.ConeModel.corner line 138
22. lemma OAI.KirchbergRordam.GenericRW.ConeModel.corner_apply line 141
23. def OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.coneHom line 156
24. lemma OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.matrixHom_single line 160
25. lemma OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.coneHom_corner line 165
26. def OAI.KirchbergRordam.GenericRW.ClosedRightRange.space line 184
27. lemma OAI.KirchbergRordam.GenericRW.ClosedRightRange.mem_space line 188
28. lemma OAI.KirchbergRordam.GenericRW.ClosedRightRange.closed line 196
29. def OAI.KirchbergRordam.GenericRW.ClosedRightRange.embed line 203
30. lemma OAI.KirchbergRordam.GenericRW.ClosedRightRange.embed_val line 206
31. lemma OAI.KirchbergRordam.GenericRW.ClosedRightRange.dense line 208
32. lemma OAI.KirchbergRordam.GenericRW.ClosedRightRange.norm_mul_eq line 226
33. def OAI.KirchbergRordam.GenericRW.ClosedRightRange.transport line 242
34. lemma OAI.KirchbergRordam.GenericRW.ClosedRightRange.transport_embed line 245
35. lemma OAI.KirchbergRordam.GenericRW.ClosedRightRange.transport_inner line 250
36. lemma OAI.KirchbergRordam.GenericRW.ClosedRightRange.transport_mem line 263
37. lemma OAI.KirchbergRordam.GenericRW.ClosedRightRange.mul_right_mem line 270
38. lemma OAI.KirchbergRordam.GenericRW.ClosedRightRange.space_le line 279
39. lemma OAI.KirchbergRordam.GenericRW.ClosedRightRange.space_mul_le line 284
40. def OAI.KirchbergRordam.GenericRW.ClosedRightRange.hereditary line 287
41. lemma OAI.KirchbergRordam.GenericRW.ClosedRightRange.self_mul_star_mem_hereditary line 289
42. def OAI.KirchbergRordam.GenericRW.HereditaryTransport.raw line 308
43. abbrev OAI.KirchbergRordam.GenericRW.HereditaryTransport.corner line 316
44. instance OAI.KirchbergRordam.GenericRW.HereditaryTransport.cornerClosed line 318
45. instance OAI.KirchbergRordam.GenericRW.HereditaryTransport.(instance at line 320) line 320
46. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.mem_corner line 323
47. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.corner_eq line 331
48. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.in_space line 337
49. def OAI.KirchbergRordam.GenericRW.HereditaryTransport.embed line 344
50. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.dense line 346
51. def OAI.KirchbergRordam.GenericRW.HereditaryTransport.left line 364
52. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.continuous_left line 366
53. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.left_embed line 371
54. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.star_left_mem line 377
55. def OAI.KirchbergRordam.GenericRW.HereditaryTransport.conjugate line 384
56. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.continuous_conjugate line 387
57. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.conjugate_embed line 391
58. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.conjugate_add line 400
59. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.conjugate_zero line 410
60. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.conjugate_smul line 414
61. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.conjugate_mul line 424
62. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.conjugate_star line 437
63. def OAI.KirchbergRordam.GenericRW.HereditaryTransport.hom line 447
64. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.left_inner line 455
65. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.hom_inner line 458
66. def OAI.KirchbergRordam.GenericRW.Vanish.algebra line 477
67. instance OAI.KirchbergRordam.GenericRW.Vanish.closed line 485
68. abbrev OAI.KirchbergRordam.GenericRW.Vanish.Functions line 491
69. instance OAI.KirchbergRordam.GenericRW.Vanish.(instance at line 493) line 493
70. def OAI.KirchbergRordam.GenericRW.Vanish.multiplier line 496
71. lemma OAI.KirchbergRordam.GenericRW.Vanish.multiplier_apply line 503
72. lemma OAI.KirchbergRordam.GenericRW.Vanish.multiplier_dense line 511