OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources2.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA64 line 16
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB64 line 17
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC64 line 18
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm64 line 19
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq64 line 21
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA65 line 72
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB65 line 73
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC65 line 74
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm65 line 75
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq65 line 77
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA66 line 128
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB66 line 129
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC66 line 130
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm66 line 131
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq66 line 133
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA67 line 322
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB67 line 323
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC67 line 324
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm67 line 325
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq67 line 327
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA68 line 516
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB68 line 517
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC68 line 518
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm68 line 519
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq68 line 521
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA69 line 572
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB69 line 573
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC69 line 574
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm69 line 575
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq69 line 577
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA70 line 628
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB70 line 629
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC70 line 630
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm70 line 631
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq70 line 633
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA71 line 684
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB71 line 685
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC71 line 686
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm71 line 687
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq71 line 689
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA72 line 878
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB72 line 879
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC72 line 880
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm72 line 881
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq72 line 883
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA73 line 1072
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB73 line 1073
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC73 line 1074
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm73 line 1075
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq73 line 1077
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA74 line 1266
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB74 line 1267
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC74 line 1268
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm74 line 1269
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq74 line 1271
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA75 line 1322
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB75 line 1323
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC75 line 1324
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm75 line 1325
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq75 line 1327
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA76 line 1378
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB76 line 1379
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC76 line 1380
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm76 line 1381
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq76 line 1383
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA77 line 1434
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB77 line 1435
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC77 line 1436
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm77 line 1437
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq77 line 1439
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA78 line 1490
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB78 line 1491
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC78 line 1492
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm78 line 1493
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq78 line 1495
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA79 line 1546
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB79 line 1547
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC79 line 1548
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm79 line 1549
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq79 line 1551
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA80 line 1602
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB80 line 1603
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC80 line 1604
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm80 line 1605
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq80 line 1607
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA81 line 1658
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB81 line 1659
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC81 line 1660
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm81 line 1661
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq81 line 1663
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA82 line 1714
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB82 line 1715
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC82 line 1716
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm82 line 1717
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq82 line 1719
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA83 line 1770
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB83 line 1771
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC83 line 1772
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm83 line 1773
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq83 line 1775
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA84 line 1964
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB84 line 1965
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC84 line 1966
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm84 line 1967
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq84 line 1969
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA85 line 2158
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB85 line 2159
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC85 line 2160
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm85 line 2161
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq85 line 2163
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA86 line 2214
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB86 line 2215
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC86 line 2216
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm86 line 2217
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq86 line 2219
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA87 line 2270
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB87 line 2271
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC87 line 2272
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm87 line 2273
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq87 line 2275
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA88 line 2326
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB88 line 2327
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC88 line 2328
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm88 line 2329
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq88 line 2331
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA89 line 2382
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB89 line 2383
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC89 line 2384
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm89 line 2385
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq89 line 2387
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA90 line 2438
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB90 line 2439
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC90 line 2440
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm90 line 2441
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq90 line 2443
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA91 line 2494
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB91 line 2495
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC91 line 2496
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm91 line 2497
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq91 line 2499
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA92 line 2550
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB92 line 2551
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC92 line 2552
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm92 line 2553
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq92 line 2555
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA93 line 2744
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB93 line 2745
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC93 line 2746
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm93 line 2747
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq93 line 2749
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA94 line 2938
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB94 line 2939
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC94 line 2940
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm94 line 2941
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq94 line 2943
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA95 line 3132
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB95 line 3133
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC95 line 3134
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm95 line 3135
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq95 line 3137