OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources70.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA2240 line 38
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB2240 line 39
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC2240 line 40
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2240 line 41
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2240 line 43
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA2241 line 94
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB2241 line 95
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC2241 line 96
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2241 line 97
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2241 line 99
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA2242 line 288
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB2242 line 289
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC2242 line 290
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2242 line 291
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2242 line 293
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA2243 line 344
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB2243 line 345
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC2243 line 346
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2243 line 347
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2243 line 349
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA2244 line 400
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB2244 line 401
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC2244 line 402
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2244 line 403
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2244 line 405
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA2245 line 456
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB2245 line 457
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC2245 line 458
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2245 line 459
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2245 line 461
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA2246 line 512
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB2246 line 513
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC2246 line 514
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2246 line 515
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2246 line 517
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA2247 line 568
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB2247 line 569
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC2247 line 570
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2247 line 571
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2247 line 573
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA2248 line 624
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB2248 line 625
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC2248 line 626
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2248 line 627
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2248 line 629
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA2249 line 680
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB2249 line 681
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC2249 line 682
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2249 line 683
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2249 line 685
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA2250 line 874
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB2250 line 875
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC2250 line 876
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2250 line 877
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2250 line 879
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA2251 line 1068
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB2251 line 1069
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC2251 line 1070
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2251 line 1071
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2251 line 1073
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA2252 line 1262
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB2252 line 1263
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC2252 line 1264
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2252 line 1265
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2252 line 1267
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA2253 line 1456
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB2253 line 1457
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC2253 line 1458
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2253 line 1459
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2253 line 1461
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA2254 line 1650
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB2254 line 1651
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC2254 line 1652
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2254 line 1653
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2254 line 1655
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA2255 line 1706
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB2255 line 1707
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC2255 line 1708
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2255 line 1709
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2255 line 1711
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA2256 line 1762
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB2256 line 1763
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC2256 line 1764
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2256 line 1765
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2256 line 1767
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA2257 line 1956
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB2257 line 1957
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC2257 line 1958
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2257 line 1959
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2257 line 1961
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA2258 line 2150
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB2258 line 2151
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC2258 line 2152
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2258 line 2153
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2258 line 2155
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA2259 line 2344
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB2259 line 2345
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC2259 line 2346
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2259 line 2347
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2259 line 2349
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA2260 line 2538
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB2260 line 2539
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC2260 line 2540
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2260 line 2541
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2260 line 2543
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA2261 line 2732
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB2261 line 2733
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC2261 line 2734
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2261 line 2735
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2261 line 2737
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA2262 line 2926
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB2262 line 2927
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC2262 line 2928
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2262 line 2929
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2262 line 2931
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA2263 line 3120
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB2263 line 3121
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC2263 line 3122
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2263 line 3123
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2263 line 3125
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA2264 line 3314
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB2264 line 3315
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC2264 line 3316
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2264 line 3317
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2264 line 3319
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA2265 line 3370
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB2265 line 3371
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC2265 line 3372
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2265 line 3373
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2265 line 3375
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA2266 line 3426
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB2266 line 3427
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC2266 line 3428
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2266 line 3429
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2266 line 3431
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA2267 line 3620
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB2267 line 3621
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC2267 line 3622
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2267 line 3623
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2267 line 3625
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA2268 line 3814
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB2268 line 3815
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC2268 line 3816
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2268 line 3817
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2268 line 3819
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA2269 line 4008
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB2269 line 4009
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC2269 line 4010
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2269 line 4011
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2269 line 4013
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA2270 line 4202
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB2270 line 4203
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC2270 line 4204
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2270 line 4205
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2270 line 4207
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA2271 line 4258
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB2271 line 4259
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC2271 line 4260
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2271 line 4261
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2271 line 4263