OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources8.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA256 line 17
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB256 line 18
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC256 line 19
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm256 line 20
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq256 line 22
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA257 line 73
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB257 line 74
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC257 line 75
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm257 line 76
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq257 line 78
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA258 line 129
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB258 line 130
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC258 line 131
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm258 line 132
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq258 line 134
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA259 line 185
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB259 line 186
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC259 line 187
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm259 line 188
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq259 line 190
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA260 line 241
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB260 line 242
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC260 line 243
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm260 line 244
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq260 line 246
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA261 line 297
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB261 line 298
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC261 line 299
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm261 line 300
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq261 line 302
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA262 line 353
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB262 line 354
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC262 line 355
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm262 line 356
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq262 line 358
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA263 line 409
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB263 line 410
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC263 line 411
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm263 line 412
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq263 line 414
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA264 line 465
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB264 line 466
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC264 line 467
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm264 line 468
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq264 line 470
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA265 line 521
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB265 line 522
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC265 line 523
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm265 line 524
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq265 line 526
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA266 line 577
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB266 line 578
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC266 line 579
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm266 line 580
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq266 line 582
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA267 line 771
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB267 line 772
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC267 line 773
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm267 line 774
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq267 line 776
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA268 line 965
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB268 line 966
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC268 line 967
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm268 line 968
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq268 line 970
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA269 line 1159
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB269 line 1160
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC269 line 1161
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm269 line 1162
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq269 line 1164
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA270 line 1215
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB270 line 1216
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC270 line 1217
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm270 line 1218
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq270 line 1220
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA271 line 1271
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB271 line 1272
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC271 line 1273
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm271 line 1274
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq271 line 1276
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA272 line 1327
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB272 line 1328
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC272 line 1329
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm272 line 1330
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq272 line 1332
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA273 line 1383
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB273 line 1384
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC273 line 1385
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm273 line 1386
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq273 line 1388
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA274 line 1439
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB274 line 1440
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC274 line 1441
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm274 line 1442
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq274 line 1444
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA275 line 1495
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB275 line 1496
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC275 line 1497
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm275 line 1498
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq275 line 1500
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA276 line 1551
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB276 line 1552
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC276 line 1553
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm276 line 1554
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq276 line 1556
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA277 line 1607
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB277 line 1608
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC277 line 1609
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm277 line 1610
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq277 line 1612
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA278 line 1663
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB278 line 1664
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC278 line 1665
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm278 line 1666
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq278 line 1668
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA279 line 1857
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB279 line 1858
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC279 line 1859
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm279 line 1860
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq279 line 1862
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA280 line 2051
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB280 line 2052
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC280 line 2053
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm280 line 2054
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq280 line 2056
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA281 line 2245
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB281 line 2246
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC281 line 2247
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm281 line 2248
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq281 line 2250
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA282 line 2301
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB282 line 2302
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC282 line 2303
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm282 line 2304
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq282 line 2306
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA283 line 2357
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB283 line 2358
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC283 line 2359
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm283 line 2360
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq283 line 2362
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA284 line 2413
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB284 line 2414
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC284 line 2415
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm284 line 2416
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq284 line 2418
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA285 line 2469
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB285 line 2470
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC285 line 2471
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm285 line 2472
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq285 line 2474
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA286 line 2525
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB286 line 2526
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC286 line 2527
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm286 line 2528
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq286 line 2530
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA287 line 2581
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB287 line 2582
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC287 line 2583
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm287 line 2584
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq287 line 2586