OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources17.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA544 line 32
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB544 line 33
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC544 line 34
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm544 line 35
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq544 line 37
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA545 line 226
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB545 line 227
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC545 line 228
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm545 line 229
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq545 line 231
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA546 line 282
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB546 line 283
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC546 line 284
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm546 line 285
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq546 line 287
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA547 line 338
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB547 line 339
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC547 line 340
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm547 line 341
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq547 line 343
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA548 line 394
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB548 line 395
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC548 line 396
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm548 line 397
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq548 line 399
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA549 line 450
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB549 line 451
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC549 line 452
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm549 line 453
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq549 line 455
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA550 line 644
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB550 line 645
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC550 line 646
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm550 line 647
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq550 line 649
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA551 line 838
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB551 line 839
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC551 line 840
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm551 line 841
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq551 line 843
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA552 line 1032
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB552 line 1033
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC552 line 1034
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm552 line 1035
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq552 line 1037
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA553 line 1088
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB553 line 1089
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC553 line 1090
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm553 line 1091
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq553 line 1093
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA554 line 1144
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB554 line 1145
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC554 line 1146
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm554 line 1147
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq554 line 1149
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA555 line 1200
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB555 line 1201
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC555 line 1202
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm555 line 1203
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq555 line 1205
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA556 line 1256
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB556 line 1257
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC556 line 1258
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm556 line 1259
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq556 line 1261
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA557 line 1312
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB557 line 1313
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC557 line 1314
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm557 line 1315
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq557 line 1317
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA558 line 1368
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB558 line 1369
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC558 line 1370
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm558 line 1371
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq558 line 1373
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA559 line 1562
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB559 line 1563
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC559 line 1564
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm559 line 1565
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq559 line 1567
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA560 line 1756
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB560 line 1757
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC560 line 1758
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm560 line 1759
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq560 line 1761
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA561 line 1950
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB561 line 1951
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC561 line 1952
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm561 line 1953
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq561 line 1955
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA562 line 2006
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB562 line 2007
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC562 line 2008
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm562 line 2009
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq562 line 2011
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA563 line 2062
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB563 line 2063
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC563 line 2064
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm563 line 2065
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq563 line 2067
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA564 line 2118
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB564 line 2119
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC564 line 2120
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm564 line 2121
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq564 line 2123
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA565 line 2312
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB565 line 2313
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC565 line 2314
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm565 line 2315
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq565 line 2317
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA566 line 2506
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB566 line 2507
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC566 line 2508
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm566 line 2509
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq566 line 2511
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA567 line 2700
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB567 line 2701
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC567 line 2702
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm567 line 2703
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq567 line 2705
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA568 line 2756
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB568 line 2757
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC568 line 2758
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm568 line 2759
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq568 line 2761
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA569 line 2812
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB569 line 2813
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC569 line 2814
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm569 line 2815
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq569 line 2817
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA570 line 2868
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB570 line 2869
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC570 line 2870
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm570 line 2871
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq570 line 2873
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA571 line 2924
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB571 line 2925
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC571 line 2926
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm571 line 2927
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq571 line 2929
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA572 line 2980
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB572 line 2981
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC572 line 2982
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm572 line 2983
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq572 line 2985
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA573 line 3174
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB573 line 3175
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC573 line 3176
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm573 line 3177
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq573 line 3179
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA574 line 3368
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB574 line 3369
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC574 line 3370
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm574 line 3371
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq574 line 3373
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA575 line 3562
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB575 line 3563
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC575 line 3564
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm575 line 3565
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq575 line 3567