OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources16.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA512 line 27
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB512 line 28
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC512 line 29
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm512 line 30
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq512 line 32
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA513 line 221
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB513 line 222
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC513 line 223
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm513 line 224
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq513 line 226
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA514 line 277
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB514 line 278
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC514 line 279
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm514 line 280
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq514 line 282
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA515 line 333
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB515 line 334
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC515 line 335
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm515 line 336
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq515 line 338
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA516 line 389
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB516 line 390
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC516 line 391
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm516 line 392
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq516 line 394
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA517 line 445
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB517 line 446
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC517 line 447
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm517 line 448
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq517 line 450
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA518 line 501
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB518 line 502
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC518 line 503
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm518 line 504
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq518 line 506
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA519 line 557
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB519 line 558
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC519 line 559
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm519 line 560
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq519 line 562
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA520 line 613
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB520 line 614
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC520 line 615
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm520 line 616
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq520 line 618
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA521 line 669
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB521 line 670
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC521 line 671
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm521 line 672
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq521 line 674
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA522 line 725
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB522 line 726
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC522 line 727
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm522 line 728
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq522 line 730
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA523 line 919
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB523 line 920
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC523 line 921
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm523 line 922
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq523 line 924
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA524 line 1113
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB524 line 1114
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC524 line 1115
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm524 line 1116
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq524 line 1118
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA525 line 1307
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB525 line 1308
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC525 line 1309
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm525 line 1310
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq525 line 1312
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA526 line 1363
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB526 line 1364
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC526 line 1365
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm526 line 1366
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq526 line 1368
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA527 line 1419
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB527 line 1420
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC527 line 1421
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm527 line 1422
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq527 line 1424
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA528 line 1475
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB528 line 1476
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC528 line 1477
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm528 line 1478
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq528 line 1480
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA529 line 1531
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB529 line 1532
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC529 line 1533
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm529 line 1534
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq529 line 1536
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA530 line 1587
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB530 line 1588
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC530 line 1589
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm530 line 1590
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq530 line 1592
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA531 line 1781
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB531 line 1782
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC531 line 1783
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm531 line 1784
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq531 line 1786
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA532 line 1975
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB532 line 1976
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC532 line 1977
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm532 line 1978
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq532 line 1980
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA533 line 2169
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB533 line 2170
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC533 line 2171
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm533 line 2172
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq533 line 2174
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA534 line 2363
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB534 line 2364
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC534 line 2365
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm534 line 2366
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq534 line 2368
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA535 line 2557
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB535 line 2558
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC535 line 2559
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm535 line 2560
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq535 line 2562
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA536 line 2613
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB536 line 2614
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC536 line 2615
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm536 line 2616
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq536 line 2618
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA537 line 2669
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB537 line 2670
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC537 line 2671
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm537 line 2672
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq537 line 2674
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA538 line 2725
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB538 line 2726
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC538 line 2727
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm538 line 2728
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq538 line 2730
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA539 line 2919
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB539 line 2920
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC539 line 2921
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm539 line 2922
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq539 line 2924
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA540 line 3113
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB540 line 3114
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC540 line 3115
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm540 line 3116
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq540 line 3118
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA541 line 3307
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB541 line 3308
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC541 line 3309
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm541 line 3310
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq541 line 3312
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA542 line 3363
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB542 line 3364
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC542 line 3365
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm542 line 3366
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq542 line 3368
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA543 line 3557
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB543 line 3558
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC543 line 3559
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm543 line 3560
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq543 line 3562