OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources9.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA288 line 18
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB288 line 19
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC288 line 20
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm288 line 21
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq288 line 23
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA289 line 74
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB289 line 75
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC289 line 76
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm289 line 77
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq289 line 79
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA290 line 130
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB290 line 131
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC290 line 132
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm290 line 133
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq290 line 135
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA291 line 324
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB291 line 325
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC291 line 326
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm291 line 327
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq291 line 329
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA292 line 518
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB292 line 519
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC292 line 520
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm292 line 521
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq292 line 523
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA293 line 712
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB293 line 713
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC293 line 714
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm293 line 715
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq293 line 717
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA294 line 768
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB294 line 769
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC294 line 770
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm294 line 771
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq294 line 773
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA295 line 824
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB295 line 825
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC295 line 826
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm295 line 827
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq295 line 829
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA296 line 880
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB296 line 881
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC296 line 882
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm296 line 883
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq296 line 885
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA297 line 936
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB297 line 937
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC297 line 938
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm297 line 939
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq297 line 941
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA298 line 992
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB298 line 993
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC298 line 994
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm298 line 995
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq298 line 997
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA299 line 1048
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB299 line 1049
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC299 line 1050
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm299 line 1051
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq299 line 1053
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA300 line 1104
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB300 line 1105
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC300 line 1106
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm300 line 1107
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq300 line 1109
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA301 line 1160
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB301 line 1161
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC301 line 1162
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm301 line 1163
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq301 line 1165
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA302 line 1216
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB302 line 1217
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC302 line 1218
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm302 line 1219
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq302 line 1221
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA303 line 1410
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB303 line 1411
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC303 line 1412
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm303 line 1413
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq303 line 1415
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA304 line 1604
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB304 line 1605
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC304 line 1606
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm304 line 1607
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq304 line 1609
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA305 line 1798
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB305 line 1799
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC305 line 1800
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm305 line 1801
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq305 line 1803
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA306 line 1854
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB306 line 1855
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC306 line 1856
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm306 line 1857
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq306 line 1859
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA307 line 1910
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB307 line 1911
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC307 line 1912
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm307 line 1913
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq307 line 1915
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA308 line 1966
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB308 line 1967
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC308 line 1968
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm308 line 1969
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq308 line 1971
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA309 line 2022
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB309 line 2023
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC309 line 2024
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm309 line 2025
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq309 line 2027
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA310 line 2078
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB310 line 2079
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC310 line 2080
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm310 line 2081
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq310 line 2083
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA311 line 2134
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB311 line 2135
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC311 line 2136
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm311 line 2137
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq311 line 2139
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA312 line 2190
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB312 line 2191
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC312 line 2192
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm312 line 2193
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq312 line 2195
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA313 line 2246
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB313 line 2247
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC313 line 2248
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm313 line 2249
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq313 line 2251
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA314 line 2302
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB314 line 2303
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC314 line 2304
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm314 line 2305
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq314 line 2307
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA315 line 2358
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB315 line 2359
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC315 line 2360
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm315 line 2361
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq315 line 2363
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA316 line 2414
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB316 line 2415
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC316 line 2416
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm316 line 2417
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq316 line 2419
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA317 line 2608
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB317 line 2609
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC317 line 2610
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm317 line 2611
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq317 line 2613
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA318 line 2802
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB318 line 2803
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC318 line 2804
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm318 line 2805
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq318 line 2807
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA319 line 2996
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB319 line 2997
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC319 line 2998
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm319 line 2999
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq319 line 3001