OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources69.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA2208 line 30
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB2208 line 31
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC2208 line 32
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2208 line 33
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2208 line 35
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA2209 line 86
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB2209 line 87
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC2209 line 88
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2209 line 89
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2209 line 91
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA2210 line 142
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB2210 line 143
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC2210 line 144
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2210 line 145
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2210 line 147
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA2211 line 336
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB2211 line 337
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC2211 line 338
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2211 line 339
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2211 line 341
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA2212 line 530
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB2212 line 531
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC2212 line 532
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2212 line 533
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2212 line 535
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA2213 line 586
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB2213 line 587
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC2213 line 588
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2213 line 589
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2213 line 591
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA2214 line 780
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB2214 line 781
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC2214 line 782
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2214 line 783
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2214 line 785
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA2215 line 974
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB2215 line 975
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC2215 line 976
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2215 line 977
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2215 line 979
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA2216 line 1168
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB2216 line 1169
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC2216 line 1170
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2216 line 1171
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2216 line 1173
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA2217 line 1362
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB2217 line 1363
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC2217 line 1364
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2217 line 1365
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2217 line 1367
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA2218 line 1556
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB2218 line 1557
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC2218 line 1558
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2218 line 1559
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2218 line 1561
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA2219 line 1750
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB2219 line 1751
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC2219 line 1752
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2219 line 1753
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2219 line 1755
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA2220 line 1806
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB2220 line 1807
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC2220 line 1808
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2220 line 1809
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2220 line 1811
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA2221 line 2000
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB2221 line 2001
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC2221 line 2002
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2221 line 2003
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2221 line 2005
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA2222 line 2194
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB2222 line 2195
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC2222 line 2196
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2222 line 2197
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2222 line 2199
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA2223 line 2388
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB2223 line 2389
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC2223 line 2390
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2223 line 2391
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2223 line 2393
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA2224 line 2582
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB2224 line 2583
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC2224 line 2584
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2224 line 2585
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2224 line 2587
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA2225 line 2638
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB2225 line 2639
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC2225 line 2640
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2225 line 2641
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2225 line 2643
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA2226 line 2694
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB2226 line 2695
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC2226 line 2696
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2226 line 2697
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2226 line 2699
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA2227 line 2750
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB2227 line 2751
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC2227 line 2752
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2227 line 2753
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2227 line 2755
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA2228 line 2806
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB2228 line 2807
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC2228 line 2808
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2228 line 2809
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2228 line 2811
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA2229 line 2862
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB2229 line 2863
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC2229 line 2864
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2229 line 2865
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2229 line 2867
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA2230 line 3056
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB2230 line 3057
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC2230 line 3058
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2230 line 3059
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2230 line 3061
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA2231 line 3250
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB2231 line 3251
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC2231 line 3252
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2231 line 3253
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2231 line 3255
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA2232 line 3306
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB2232 line 3307
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC2232 line 3308
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2232 line 3309
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2232 line 3311
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA2233 line 3500
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB2233 line 3501
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC2233 line 3502
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2233 line 3503
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2233 line 3505
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA2234 line 3694
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB2234 line 3695
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC2234 line 3696
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2234 line 3697
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2234 line 3699
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA2235 line 3888
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB2235 line 3889
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC2235 line 3890
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2235 line 3891
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2235 line 3893
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA2236 line 4082
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB2236 line 4083
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC2236 line 4084
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2236 line 4085
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2236 line 4087
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA2237 line 4276
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB2237 line 4277
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC2237 line 4278
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2237 line 4279
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2237 line 4281
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA2238 line 4332
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB2238 line 4333
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC2238 line 4334
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2238 line 4335
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2238 line 4337
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA2239 line 4526
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB2239 line 4527
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC2239 line 4528
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2239 line 4529
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2239 line 4531