OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources39.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA1248 line 28
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB1248 line 29
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC1248 line 30
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1248 line 31
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1248 line 33
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA1249 line 84
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB1249 line 85
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC1249 line 86
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1249 line 87
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1249 line 89
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA1250 line 140
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB1250 line 141
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC1250 line 142
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1250 line 143
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1250 line 145
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA1251 line 196
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB1251 line 197
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC1251 line 198
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1251 line 199
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1251 line 201
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA1252 line 252
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB1252 line 253
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC1252 line 254
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1252 line 255
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1252 line 257
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA1253 line 308
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB1253 line 309
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC1253 line 310
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1253 line 311
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1253 line 313
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA1254 line 364
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB1254 line 365
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC1254 line 366
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1254 line 367
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1254 line 369
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA1255 line 420
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB1255 line 421
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC1255 line 422
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1255 line 423
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1255 line 425
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA1256 line 476
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB1256 line 477
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC1256 line 478
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1256 line 479
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1256 line 481
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA1257 line 532
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB1257 line 533
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC1257 line 534
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1257 line 535
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1257 line 537
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA1258 line 588
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB1258 line 589
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC1258 line 590
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1258 line 591
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1258 line 593
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA1259 line 644
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB1259 line 645
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC1259 line 646
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1259 line 647
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1259 line 649
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA1260 line 700
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB1260 line 701
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC1260 line 702
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1260 line 703
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1260 line 705
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA1261 line 756
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB1261 line 757
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC1261 line 758
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1261 line 759
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1261 line 761
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA1262 line 812
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB1262 line 813
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC1262 line 814
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1262 line 815
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1262 line 817
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA1263 line 868
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB1263 line 869
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC1263 line 870
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1263 line 871
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1263 line 873
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA1264 line 1062
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB1264 line 1063
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC1264 line 1064
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1264 line 1065
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1264 line 1067
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA1265 line 1256
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB1265 line 1257
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC1265 line 1258
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1265 line 1259
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1265 line 1261
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA1266 line 1450
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB1266 line 1451
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC1266 line 1452
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1266 line 1453
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1266 line 1455
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA1267 line 1644
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB1267 line 1645
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC1267 line 1646
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1267 line 1647
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1267 line 1649
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA1268 line 1838
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB1268 line 1839
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC1268 line 1840
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1268 line 1841
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1268 line 1843
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA1269 line 2032
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB1269 line 2033
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC1269 line 2034
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1269 line 2035
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1269 line 2037
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA1270 line 2088
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB1270 line 2089
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC1270 line 2090
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1270 line 2091
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1270 line 2093
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA1271 line 2144
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB1271 line 2145
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC1271 line 2146
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1271 line 2147
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1271 line 2149
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA1272 line 2200
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB1272 line 2201
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC1272 line 2202
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1272 line 2203
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1272 line 2205
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA1273 line 2394
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB1273 line 2395
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC1273 line 2396
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1273 line 2397
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1273 line 2399
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA1274 line 2588
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB1274 line 2589
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC1274 line 2590
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1274 line 2591
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1274 line 2593
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA1275 line 2782
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB1275 line 2783
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC1275 line 2784
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1275 line 2785
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1275 line 2787
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA1276 line 2838
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB1276 line 2839
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC1276 line 2840
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1276 line 2841
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1276 line 2843
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA1277 line 2894
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB1277 line 2895
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC1277 line 2896
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1277 line 2897
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1277 line 2899
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA1278 line 2950
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB1278 line 2951
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC1278 line 2952
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1278 line 2953
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1278 line 2955
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA1279 line 3144
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB1279 line 3145
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC1279 line 3146
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1279 line 3147
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1279 line 3149