OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources12.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA384 line 28
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB384 line 29
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC384 line 30
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm384 line 31
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq384 line 33
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA385 line 84
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB385 line 85
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC385 line 86
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm385 line 87
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq385 line 89
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA386 line 140
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB386 line 141
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC386 line 142
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm386 line 143
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq386 line 145
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA387 line 196
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB387 line 197
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC387 line 198
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm387 line 199
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq387 line 201
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA388 line 252
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB388 line 253
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC388 line 254
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm388 line 255
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq388 line 257
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA389 line 308
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB389 line 309
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC389 line 310
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm389 line 311
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq389 line 313
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA390 line 502
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB390 line 503
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC390 line 504
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm390 line 505
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq390 line 507
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA391 line 696
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB391 line 697
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC391 line 698
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm391 line 699
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq391 line 701
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA392 line 890
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB392 line 891
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC392 line 892
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm392 line 893
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq392 line 895
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA393 line 946
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB393 line 947
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC393 line 948
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm393 line 949
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq393 line 951
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA394 line 1002
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB394 line 1003
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC394 line 1004
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm394 line 1005
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq394 line 1007
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA395 line 1058
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB395 line 1059
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC395 line 1060
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm395 line 1061
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq395 line 1063
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA396 line 1114
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB396 line 1115
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC396 line 1116
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm396 line 1117
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq396 line 1119
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA397 line 1170
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB397 line 1171
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC397 line 1172
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm397 line 1173
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq397 line 1175
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA398 line 1226
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB398 line 1227
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC398 line 1228
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm398 line 1229
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq398 line 1231
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA399 line 1420
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB399 line 1421
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC399 line 1422
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm399 line 1423
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq399 line 1425
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA400 line 1614
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB400 line 1615
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC400 line 1616
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm400 line 1617
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq400 line 1619
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA401 line 1808
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB401 line 1809
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC401 line 1810
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm401 line 1811
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq401 line 1813
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA402 line 1864
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB402 line 1865
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC402 line 1866
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm402 line 1867
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq402 line 1869
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA403 line 1920
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB403 line 1921
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC403 line 1922
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm403 line 1923
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq403 line 1925
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA404 line 1976
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB404 line 1977
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC404 line 1978
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm404 line 1979
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq404 line 1981
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA405 line 2032
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB405 line 2033
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC405 line 2034
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm405 line 2035
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq405 line 2037
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA406 line 2226
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB406 line 2227
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC406 line 2228
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm406 line 2229
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq406 line 2231
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA407 line 2420
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB407 line 2421
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC407 line 2422
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm407 line 2423
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq407 line 2425
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA408 line 2614
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB408 line 2615
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC408 line 2616
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm408 line 2617
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq408 line 2619
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA409 line 2808
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB409 line 2809
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC409 line 2810
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm409 line 2811
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq409 line 2813
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA410 line 3002
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB410 line 3003
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC410 line 3004
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm410 line 3005
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq410 line 3007
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA411 line 3196
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB411 line 3197
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC411 line 3198
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm411 line 3199
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq411 line 3201
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA412 line 3390
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB412 line 3391
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC412 line 3392
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm412 line 3393
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq412 line 3395
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA413 line 3446
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB413 line 3447
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC413 line 3448
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm413 line 3449
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq413 line 3451
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA414 line 3502
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB414 line 3503
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC414 line 3504
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm414 line 3505
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq414 line 3507
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA415 line 3558
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB415 line 3559
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC415 line 3560
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm415 line 3561
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq415 line 3563