OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources44.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA1408 line 25
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB1408 line 26
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC1408 line 27
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1408 line 28
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1408 line 30
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA1409 line 81
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB1409 line 82
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC1409 line 83
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1409 line 84
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1409 line 86
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA1410 line 137
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB1410 line 138
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC1410 line 139
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1410 line 140
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1410 line 142
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA1411 line 193
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB1411 line 194
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC1411 line 195
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1411 line 196
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1411 line 198
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA1412 line 249
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB1412 line 250
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC1412 line 251
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1412 line 252
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1412 line 254
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA1413 line 305
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB1413 line 306
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC1413 line 307
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1413 line 308
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1413 line 310
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA1414 line 361
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB1414 line 362
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC1414 line 363
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1414 line 364
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1414 line 366
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA1415 line 417
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB1415 line 418
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC1415 line 419
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1415 line 420
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1415 line 422
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA1416 line 473
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB1416 line 474
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC1416 line 475
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1416 line 476
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1416 line 478
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA1417 line 529
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB1417 line 530
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC1417 line 531
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1417 line 532
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1417 line 534
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA1418 line 585
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB1418 line 586
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC1418 line 587
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1418 line 588
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1418 line 590
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA1419 line 641
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB1419 line 642
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC1419 line 643
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1419 line 644
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1419 line 646
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA1420 line 697
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB1420 line 698
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC1420 line 699
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1420 line 700
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1420 line 702
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA1421 line 753
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB1421 line 754
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC1421 line 755
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1421 line 756
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1421 line 758
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA1422 line 809
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB1422 line 810
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC1422 line 811
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1422 line 812
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1422 line 814
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA1423 line 865
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB1423 line 866
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC1423 line 867
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1423 line 868
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1423 line 870
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA1424 line 921
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB1424 line 922
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC1424 line 923
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1424 line 924
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1424 line 926
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA1425 line 977
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB1425 line 978
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC1425 line 979
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1425 line 980
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1425 line 982
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA1426 line 1033
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB1426 line 1034
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC1426 line 1035
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1426 line 1036
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1426 line 1038
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA1427 line 1089
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB1427 line 1090
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC1427 line 1091
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1427 line 1092
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1427 line 1094
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA1428 line 1145
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB1428 line 1146
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC1428 line 1147
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1428 line 1148
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1428 line 1150
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA1429 line 1201
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB1429 line 1202
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC1429 line 1203
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1429 line 1204
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1429 line 1206
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA1430 line 1395
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB1430 line 1396
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC1430 line 1397
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1430 line 1398
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1430 line 1400
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA1431 line 1589
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB1431 line 1590
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC1431 line 1591
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1431 line 1592
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1431 line 1594
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA1432 line 1645
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB1432 line 1646
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC1432 line 1647
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1432 line 1648
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1432 line 1650
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA1433 line 1701
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB1433 line 1702
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC1433 line 1703
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1433 line 1704
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1433 line 1706
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA1434 line 1757
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB1434 line 1758
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC1434 line 1759
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1434 line 1760
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1434 line 1762
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA1435 line 1951
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB1435 line 1952
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC1435 line 1953
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1435 line 1954
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1435 line 1956
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA1436 line 2145
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB1436 line 2146
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC1436 line 2147
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1436 line 2148
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1436 line 2150
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA1437 line 2201
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB1437 line 2202
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC1437 line 2203
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1437 line 2204
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1437 line 2206
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA1438 line 2395
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB1438 line 2396
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC1438 line 2397
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1438 line 2398
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1438 line 2400
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA1439 line 2589
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB1439 line 2590
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC1439 line 2591
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1439 line 2592
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1439 line 2594