OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources7.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA224 line 16
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB224 line 17
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC224 line 18
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm224 line 19
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq224 line 21
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA225 line 72
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB225 line 73
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC225 line 74
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm225 line 75
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq225 line 77
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA226 line 128
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB226 line 129
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC226 line 130
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm226 line 131
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq226 line 133
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA227 line 184
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB227 line 185
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC227 line 186
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm227 line 187
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq227 line 189
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA228 line 240
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB228 line 241
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC228 line 242
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm228 line 243
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq228 line 245
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA229 line 296
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB229 line 297
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC229 line 298
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm229 line 299
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq229 line 301
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA230 line 352
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB230 line 353
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC230 line 354
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm230 line 355
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq230 line 357
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA231 line 408
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB231 line 409
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC231 line 410
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm231 line 411
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq231 line 413
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA232 line 464
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB232 line 465
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC232 line 466
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm232 line 467
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq232 line 469
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA233 line 658
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB233 line 659
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC233 line 660
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm233 line 661
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq233 line 663
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA234 line 852
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB234 line 853
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC234 line 854
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm234 line 855
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq234 line 857
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA235 line 1046
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB235 line 1047
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC235 line 1048
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm235 line 1049
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq235 line 1051
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA236 line 1102
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB236 line 1103
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC236 line 1104
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm236 line 1105
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq236 line 1107
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA237 line 1158
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB237 line 1159
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC237 line 1160
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm237 line 1161
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq237 line 1163
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA238 line 1214
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB238 line 1215
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC238 line 1216
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm238 line 1217
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq238 line 1219
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA239 line 1270
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB239 line 1271
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC239 line 1272
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm239 line 1273
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq239 line 1275
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA240 line 1326
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB240 line 1327
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC240 line 1328
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm240 line 1329
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq240 line 1331
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA241 line 1382
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB241 line 1383
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC241 line 1384
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm241 line 1385
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq241 line 1387
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA242 line 1438
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB242 line 1439
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC242 line 1440
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm242 line 1441
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq242 line 1443
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA243 line 1632
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB243 line 1633
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC243 line 1634
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm243 line 1635
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq243 line 1637
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA244 line 1826
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB244 line 1827
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC244 line 1828
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm244 line 1829
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq244 line 1831
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA245 line 2020
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB245 line 2021
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC245 line 2022
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm245 line 2023
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq245 line 2025
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA246 line 2076
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB246 line 2077
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC246 line 2078
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm246 line 2079
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq246 line 2081
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA247 line 2132
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB247 line 2133
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC247 line 2134
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm247 line 2135
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq247 line 2137
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA248 line 2188
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB248 line 2189
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC248 line 2190
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm248 line 2191
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq248 line 2193
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA249 line 2244
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB249 line 2245
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC249 line 2246
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm249 line 2247
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq249 line 2249
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA250 line 2300
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB250 line 2301
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC250 line 2302
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm250 line 2303
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq250 line 2305
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA251 line 2356
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB251 line 2357
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC251 line 2358
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm251 line 2359
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq251 line 2361
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA252 line 2412
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB252 line 2413
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC252 line 2414
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm252 line 2415
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq252 line 2417
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA253 line 2606
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB253 line 2607
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC253 line 2608
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm253 line 2609
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq253 line 2611
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA254 line 2800
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB254 line 2801
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC254 line 2802
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm254 line 2803
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq254 line 2805
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA255 line 2994
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB255 line 2995
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC255 line 2996
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm255 line 2997
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq255 line 2999