OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources42.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA1344 line 25
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB1344 line 26
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC1344 line 27
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1344 line 28
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1344 line 30
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA1345 line 219
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB1345 line 220
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC1345 line 221
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1345 line 222
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1345 line 224
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA1346 line 413
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB1346 line 414
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC1346 line 415
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1346 line 416
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1346 line 418
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA1347 line 607
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB1347 line 608
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC1347 line 609
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1347 line 610
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1347 line 612
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA1348 line 663
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB1348 line 664
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC1348 line 665
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1348 line 666
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1348 line 668
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA1349 line 857
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB1349 line 858
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC1349 line 859
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1349 line 860
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1349 line 862
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA1350 line 1051
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB1350 line 1052
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC1350 line 1053
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1350 line 1054
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1350 line 1056
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA1351 line 1245
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB1351 line 1246
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC1351 line 1247
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1351 line 1248
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1351 line 1250
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA1352 line 1301
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB1352 line 1302
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC1352 line 1303
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1352 line 1304
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1352 line 1306
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA1353 line 1357
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB1353 line 1358
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC1353 line 1359
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1353 line 1360
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1353 line 1362
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA1354 line 1413
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB1354 line 1414
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC1354 line 1415
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1354 line 1416
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1354 line 1418
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA1355 line 1469
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB1355 line 1470
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC1355 line 1471
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1355 line 1472
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1355 line 1474
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA1356 line 1525
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB1356 line 1526
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC1356 line 1527
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1356 line 1528
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1356 line 1530
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA1357 line 1719
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB1357 line 1720
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC1357 line 1721
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1357 line 1722
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1357 line 1724
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA1358 line 1913
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB1358 line 1914
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC1358 line 1915
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1358 line 1916
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1358 line 1918
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA1359 line 2107
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB1359 line 2108
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC1359 line 2109
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1359 line 2110
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1359 line 2112
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA1360 line 2301
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB1360 line 2302
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC1360 line 2303
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1360 line 2304
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1360 line 2306
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA1361 line 2495
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB1361 line 2496
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC1361 line 2497
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1361 line 2498
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1361 line 2500
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA1362 line 2551
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB1362 line 2552
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC1362 line 2553
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1362 line 2554
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1362 line 2556
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA1363 line 2607
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB1363 line 2608
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC1363 line 2609
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1363 line 2610
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1363 line 2612
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA1364 line 2663
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB1364 line 2664
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC1364 line 2665
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1364 line 2666
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1364 line 2668
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA1365 line 2719
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB1365 line 2720
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC1365 line 2721
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1365 line 2722
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1365 line 2724
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA1366 line 2775
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB1366 line 2776
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC1366 line 2777
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1366 line 2778
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1366 line 2780
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA1367 line 2831
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB1367 line 2832
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC1367 line 2833
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1367 line 2834
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1367 line 2836
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA1368 line 2887
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB1368 line 2888
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC1368 line 2889
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1368 line 2890
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1368 line 2892
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA1369 line 2943
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB1369 line 2944
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC1369 line 2945
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1369 line 2946
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1369 line 2948
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA1370 line 2999
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB1370 line 3000
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC1370 line 3001
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1370 line 3002
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1370 line 3004
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA1371 line 3055
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB1371 line 3056
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC1371 line 3057
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1371 line 3058
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1371 line 3060
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA1372 line 3111
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB1372 line 3112
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC1372 line 3113
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1372 line 3114
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1372 line 3116
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA1373 line 3167
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB1373 line 3168
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC1373 line 3169
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1373 line 3170
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1373 line 3172
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA1374 line 3223
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB1374 line 3224
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC1374 line 3225
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1374 line 3226
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1374 line 3228
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA1375 line 3279
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB1375 line 3280
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC1375 line 3281
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1375 line 3282
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1375 line 3284