OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources48.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA1536 line 34
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB1536 line 35
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC1536 line 36
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1536 line 37
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1536 line 39
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA1537 line 90
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB1537 line 91
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC1537 line 92
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1537 line 93
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1537 line 95
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA1538 line 146
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB1538 line 147
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC1538 line 148
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1538 line 149
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1538 line 151
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA1539 line 202
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB1539 line 203
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC1539 line 204
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1539 line 205
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1539 line 207
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA1540 line 258
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB1540 line 259
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC1540 line 260
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1540 line 261
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1540 line 263
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA1541 line 452
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB1541 line 453
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC1541 line 454
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1541 line 455
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1541 line 457
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA1542 line 646
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB1542 line 647
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC1542 line 648
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1542 line 649
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1542 line 651
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA1543 line 840
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB1543 line 841
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC1543 line 842
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1543 line 843
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1543 line 845
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA1544 line 896
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB1544 line 897
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC1544 line 898
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1544 line 899
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1544 line 901
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA1545 line 952
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB1545 line 953
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC1545 line 954
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1545 line 955
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1545 line 957
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA1546 line 1146
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB1546 line 1147
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC1546 line 1148
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1546 line 1149
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1546 line 1151
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA1547 line 1340
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB1547 line 1341
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC1547 line 1342
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1547 line 1343
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1547 line 1345
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA1548 line 1534
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB1548 line 1535
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC1548 line 1536
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1548 line 1537
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1548 line 1539
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA1549 line 1728
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB1549 line 1729
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC1549 line 1730
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1549 line 1731
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1549 line 1733
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA1550 line 1922
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB1550 line 1923
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC1550 line 1924
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1550 line 1925
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1550 line 1927
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA1551 line 2116
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB1551 line 2117
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC1551 line 2118
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1551 line 2119
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1551 line 2121
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA1552 line 2310
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB1552 line 2311
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC1552 line 2312
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1552 line 2313
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1552 line 2315
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA1553 line 2366
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB1553 line 2367
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC1553 line 2368
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1553 line 2369
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1553 line 2371
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA1554 line 2560
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB1554 line 2561
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC1554 line 2562
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1554 line 2563
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1554 line 2565
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA1555 line 2616
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB1555 line 2617
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC1555 line 2618
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1555 line 2619
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1555 line 2621
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA1556 line 2672
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB1556 line 2673
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC1556 line 2674
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1556 line 2675
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1556 line 2677
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA1557 line 2866
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB1557 line 2867
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC1557 line 2868
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1557 line 2869
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1557 line 2871
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA1558 line 3060
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB1558 line 3061
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC1558 line 3062
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1558 line 3063
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1558 line 3065
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA1559 line 3116
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB1559 line 3117
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC1559 line 3118
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1559 line 3119
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1559 line 3121
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA1560 line 3172
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB1560 line 3173
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC1560 line 3174
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1560 line 3175
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1560 line 3177
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA1561 line 3366
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB1561 line 3367
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC1561 line 3368
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1561 line 3369
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1561 line 3371
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA1562 line 3422
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB1562 line 3423
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC1562 line 3424
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1562 line 3425
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1562 line 3427
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA1563 line 3478
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB1563 line 3479
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC1563 line 3480
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1563 line 3481
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1563 line 3483
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA1564 line 3534
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB1564 line 3535
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC1564 line 3536
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1564 line 3537
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1564 line 3539
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA1565 line 3590
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB1565 line 3591
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC1565 line 3592
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1565 line 3593
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1565 line 3595
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA1566 line 3646
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB1566 line 3647
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC1566 line 3648
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1566 line 3649
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1566 line 3651
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA1567 line 3702
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB1567 line 3703
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC1567 line 3704
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1567 line 3705
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1567 line 3707