OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources45.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA1440 line 18
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB1440 line 19
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC1440 line 20
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1440 line 21
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1440 line 23
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA1441 line 74
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB1441 line 75
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC1441 line 76
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1441 line 77
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1441 line 79
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA1442 line 130
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB1442 line 131
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC1442 line 132
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1442 line 133
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1442 line 135
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA1443 line 186
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB1443 line 187
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC1443 line 188
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1443 line 189
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1443 line 191
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA1444 line 242
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB1444 line 243
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC1444 line 244
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1444 line 245
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1444 line 247
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA1445 line 298
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB1445 line 299
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC1445 line 300
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1445 line 301
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1445 line 303
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA1446 line 354
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB1446 line 355
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC1446 line 356
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1446 line 357
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1446 line 359
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA1447 line 410
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB1447 line 411
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC1447 line 412
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1447 line 413
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1447 line 415
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA1448 line 466
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB1448 line 467
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC1448 line 468
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1448 line 469
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1448 line 471
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA1449 line 522
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB1449 line 523
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC1449 line 524
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1449 line 525
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1449 line 527
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA1450 line 578
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB1450 line 579
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC1450 line 580
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1450 line 581
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1450 line 583
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA1451 line 634
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB1451 line 635
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC1451 line 636
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1451 line 637
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1451 line 639
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA1452 line 690
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB1452 line 691
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC1452 line 692
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1452 line 693
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1452 line 695
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA1453 line 746
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB1453 line 747
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC1453 line 748
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1453 line 749
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1453 line 751
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA1454 line 802
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB1454 line 803
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC1454 line 804
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1454 line 805
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1454 line 807
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA1455 line 858
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB1455 line 859
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC1455 line 860
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1455 line 861
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1455 line 863
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA1456 line 914
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB1456 line 915
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC1456 line 916
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1456 line 917
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1456 line 919
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA1457 line 970
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB1457 line 971
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC1457 line 972
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1457 line 973
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1457 line 975
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA1458 line 1026
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB1458 line 1027
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC1458 line 1028
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1458 line 1029
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1458 line 1031
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA1459 line 1082
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB1459 line 1083
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC1459 line 1084
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1459 line 1085
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1459 line 1087
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA1460 line 1138
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB1460 line 1139
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC1460 line 1140
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1460 line 1141
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1460 line 1143
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA1461 line 1194
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB1461 line 1195
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC1461 line 1196
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1461 line 1197
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1461 line 1199
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA1462 line 1250
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB1462 line 1251
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC1462 line 1252
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1462 line 1253
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1462 line 1255
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA1463 line 1306
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB1463 line 1307
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC1463 line 1308
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1463 line 1309
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1463 line 1311
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA1464 line 1362
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB1464 line 1363
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC1464 line 1364
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1464 line 1365
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1464 line 1367
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA1465 line 1418
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB1465 line 1419
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC1465 line 1420
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1465 line 1421
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1465 line 1423
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA1466 line 1474
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB1466 line 1475
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC1466 line 1476
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1466 line 1477
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1466 line 1479
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA1467 line 1530
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB1467 line 1531
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC1467 line 1532
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1467 line 1533
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1467 line 1535
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA1468 line 1586
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB1468 line 1587
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC1468 line 1588
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1468 line 1589
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1468 line 1591
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA1469 line 1642
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB1469 line 1643
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC1469 line 1644
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1469 line 1645
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1469 line 1647
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA1470 line 1698
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB1470 line 1699
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC1470 line 1700
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1470 line 1701
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1470 line 1703
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA1471 line 1754
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB1471 line 1755
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC1471 line 1756
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1471 line 1757
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1471 line 1759