OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources14.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA448 line 26
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB448 line 27
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC448 line 28
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm448 line 29
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq448 line 31
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA449 line 82
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB449 line 83
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC449 line 84
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm449 line 85
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq449 line 87
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA450 line 276
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB450 line 277
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC450 line 278
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm450 line 279
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq450 line 281
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA451 line 470
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB451 line 471
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC451 line 472
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm451 line 473
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq451 line 475
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA452 line 664
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB452 line 665
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC452 line 666
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm452 line 667
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq452 line 669
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA453 line 720
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB453 line 721
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC453 line 722
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm453 line 723
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq453 line 725
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA454 line 776
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB454 line 777
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC454 line 778
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm454 line 779
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq454 line 781
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA455 line 832
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB455 line 833
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC455 line 834
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm455 line 835
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq455 line 837
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA456 line 888
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB456 line 889
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC456 line 890
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm456 line 891
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq456 line 893
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA457 line 944
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB457 line 945
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC457 line 946
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm457 line 947
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq457 line 949
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA458 line 1000
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB458 line 1001
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC458 line 1002
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm458 line 1003
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq458 line 1005
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA459 line 1056
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB459 line 1057
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC459 line 1058
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm459 line 1059
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq459 line 1061
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA460 line 1250
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB460 line 1251
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC460 line 1252
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm460 line 1253
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq460 line 1255
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA461 line 1444
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB461 line 1445
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC461 line 1446
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm461 line 1447
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq461 line 1449
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA462 line 1638
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB462 line 1639
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC462 line 1640
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm462 line 1641
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq462 line 1643
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA463 line 1694
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB463 line 1695
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC463 line 1696
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm463 line 1697
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq463 line 1699
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA464 line 1750
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB464 line 1751
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC464 line 1752
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm464 line 1753
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq464 line 1755
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA465 line 1806
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB465 line 1807
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC465 line 1808
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm465 line 1809
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq465 line 1811
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA466 line 2000
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB466 line 2001
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC466 line 2002
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm466 line 2003
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq466 line 2005
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA467 line 2194
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB467 line 2195
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC467 line 2196
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm467 line 2197
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq467 line 2199
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA468 line 2388
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB468 line 2389
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC468 line 2390
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm468 line 2391
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq468 line 2393
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA469 line 2444
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB469 line 2445
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC469 line 2446
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm469 line 2447
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq469 line 2449
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA470 line 2500
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB470 line 2501
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC470 line 2502
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm470 line 2503
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq470 line 2505
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA471 line 2556
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB471 line 2557
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC471 line 2558
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm471 line 2559
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq471 line 2561
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA472 line 2612
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB472 line 2613
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC472 line 2614
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm472 line 2615
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq472 line 2617
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA473 line 2806
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB473 line 2807
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC473 line 2808
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm473 line 2809
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq473 line 2811
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA474 line 3000
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB474 line 3001
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC474 line 3002
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm474 line 3003
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq474 line 3005
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA475 line 3194
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB475 line 3195
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC475 line 3196
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm475 line 3197
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq475 line 3199
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA476 line 3250
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB476 line 3251
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC476 line 3252
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm476 line 3253
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq476 line 3255
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA477 line 3306
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB477 line 3307
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC477 line 3308
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm477 line 3309
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq477 line 3311
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA478 line 3362
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB478 line 3363
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC478 line 3364
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm478 line 3365
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq478 line 3367
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA479 line 3418
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB479 line 3419
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC479 line 3420
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm479 line 3421
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq479 line 3423