OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources47.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA1504 line 31
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB1504 line 32
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC1504 line 33
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1504 line 34
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1504 line 36
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA1505 line 87
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB1505 line 88
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC1505 line 89
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1505 line 90
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1505 line 92
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA1506 line 143
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB1506 line 144
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC1506 line 145
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1506 line 146
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1506 line 148
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA1507 line 199
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB1507 line 200
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC1507 line 201
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1507 line 202
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1507 line 204
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA1508 line 255
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB1508 line 256
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC1508 line 257
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1508 line 258
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1508 line 260
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA1509 line 311
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB1509 line 312
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC1509 line 313
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1509 line 314
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1509 line 316
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA1510 line 367
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB1510 line 368
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC1510 line 369
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1510 line 370
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1510 line 372
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA1511 line 561
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB1511 line 562
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC1511 line 563
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1511 line 564
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1511 line 566
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA1512 line 755
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB1512 line 756
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC1512 line 757
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1512 line 758
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1512 line 760
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA1513 line 949
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB1513 line 950
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC1513 line 951
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1513 line 952
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1513 line 954
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA1514 line 1005
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB1514 line 1006
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC1514 line 1007
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1514 line 1008
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1514 line 1010
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA1515 line 1061
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB1515 line 1062
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC1515 line 1063
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1515 line 1064
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1515 line 1066
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA1516 line 1117
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB1516 line 1118
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC1516 line 1119
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1516 line 1120
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1516 line 1122
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA1517 line 1173
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB1517 line 1174
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC1517 line 1175
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1517 line 1176
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1517 line 1178
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA1518 line 1367
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB1518 line 1368
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC1518 line 1369
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1518 line 1370
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1518 line 1372
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA1519 line 1561
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB1519 line 1562
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC1519 line 1563
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1519 line 1564
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1519 line 1566
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA1520 line 1755
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB1520 line 1756
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC1520 line 1757
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1520 line 1758
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1520 line 1760
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA1521 line 1949
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB1521 line 1950
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC1521 line 1951
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1521 line 1952
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1521 line 1954
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA1522 line 2143
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB1522 line 2144
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC1522 line 2145
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1522 line 2146
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1522 line 2148
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA1523 line 2337
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB1523 line 2338
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC1523 line 2339
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1523 line 2340
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1523 line 2342
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA1524 line 2531
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB1524 line 2532
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC1524 line 2533
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1524 line 2534
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1524 line 2536
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA1525 line 2725
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB1525 line 2726
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC1525 line 2727
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1525 line 2728
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1525 line 2730
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA1526 line 2781
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB1526 line 2782
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC1526 line 2783
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1526 line 2784
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1526 line 2786
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA1527 line 2837
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB1527 line 2838
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC1527 line 2839
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1527 line 2840
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1527 line 2842
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA1528 line 2893
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB1528 line 2894
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC1528 line 2895
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1528 line 2896
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1528 line 2898
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA1529 line 2949
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB1529 line 2950
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC1529 line 2951
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1529 line 2952
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1529 line 2954
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA1530 line 3143
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB1530 line 3144
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC1530 line 3145
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1530 line 3146
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1530 line 3148
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA1531 line 3337
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB1531 line 3338
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC1531 line 3339
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1531 line 3340
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1531 line 3342
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA1532 line 3531
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB1532 line 3532
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC1532 line 3533
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1532 line 3534
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1532 line 3536
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA1533 line 3725
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB1533 line 3726
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC1533 line 3727
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1533 line 3728
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1533 line 3730
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA1534 line 3919
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB1534 line 3920
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC1534 line 3921
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1534 line 3922
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1534 line 3924
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA1535 line 3975
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB1535 line 3976
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC1535 line 3977
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1535 line 3978
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1535 line 3980