OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources38.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA1216 line 21
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB1216 line 22
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC1216 line 23
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1216 line 24
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1216 line 26
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA1217 line 77
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB1217 line 78
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC1217 line 79
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1217 line 80
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1217 line 82
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA1218 line 133
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB1218 line 134
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC1218 line 135
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1218 line 136
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1218 line 138
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA1219 line 189
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB1219 line 190
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC1219 line 191
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1219 line 192
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1219 line 194
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA1220 line 245
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB1220 line 246
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC1220 line 247
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1220 line 248
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1220 line 250
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA1221 line 301
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB1221 line 302
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC1221 line 303
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1221 line 304
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1221 line 306
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA1222 line 357
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB1222 line 358
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC1222 line 359
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1222 line 360
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1222 line 362
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA1223 line 413
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB1223 line 414
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC1223 line 415
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1223 line 416
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1223 line 418
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA1224 line 469
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB1224 line 470
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC1224 line 471
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1224 line 472
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1224 line 474
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA1225 line 525
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB1225 line 526
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC1225 line 527
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1225 line 528
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1225 line 530
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA1226 line 581
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB1226 line 582
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC1226 line 583
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1226 line 584
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1226 line 586
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA1227 line 637
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB1227 line 638
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC1227 line 639
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1227 line 640
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1227 line 642
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA1228 line 693
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB1228 line 694
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC1228 line 695
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1228 line 696
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1228 line 698
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA1229 line 749
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB1229 line 750
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC1229 line 751
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1229 line 752
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1229 line 754
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA1230 line 805
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB1230 line 806
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC1230 line 807
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1230 line 808
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1230 line 810
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA1231 line 861
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB1231 line 862
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC1231 line 863
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1231 line 864
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1231 line 866
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA1232 line 917
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB1232 line 918
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC1232 line 919
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1232 line 920
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1232 line 922
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA1233 line 973
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB1233 line 974
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC1233 line 975
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1233 line 976
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1233 line 978
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA1234 line 1029
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB1234 line 1030
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC1234 line 1031
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1234 line 1032
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1234 line 1034
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA1235 line 1085
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB1235 line 1086
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC1235 line 1087
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1235 line 1088
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1235 line 1090
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA1236 line 1141
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB1236 line 1142
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC1236 line 1143
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1236 line 1144
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1236 line 1146
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA1237 line 1197
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB1237 line 1198
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC1237 line 1199
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1237 line 1200
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1237 line 1202
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA1238 line 1253
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB1238 line 1254
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC1238 line 1255
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1238 line 1256
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1238 line 1258
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA1239 line 1309
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB1239 line 1310
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC1239 line 1311
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1239 line 1312
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1239 line 1314
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA1240 line 1365
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB1240 line 1366
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC1240 line 1367
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1240 line 1368
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1240 line 1370
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA1241 line 1421
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB1241 line 1422
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC1241 line 1423
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1241 line 1424
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1241 line 1426
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA1242 line 1477
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB1242 line 1478
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC1242 line 1479
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1242 line 1480
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1242 line 1482
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA1243 line 1533
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB1243 line 1534
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC1243 line 1535
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1243 line 1536
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1243 line 1538
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA1244 line 1589
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB1244 line 1590
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC1244 line 1591
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1244 line 1592
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1244 line 1594
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA1245 line 1645
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB1245 line 1646
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC1245 line 1647
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1245 line 1648
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1245 line 1650
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA1246 line 1701
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB1246 line 1702
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC1246 line 1703
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1246 line 1704
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1246 line 1706
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA1247 line 1757
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB1247 line 1758
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC1247 line 1759
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1247 line 1760
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1247 line 1762