OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources10.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA320 line 19
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB320 line 20
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC320 line 21
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm320 line 22
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq320 line 24
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA321 line 75
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB321 line 76
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC321 line 77
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm321 line 78
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq321 line 80
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA322 line 131
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB322 line 132
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC322 line 133
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm322 line 134
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq322 line 136
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA323 line 187
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB323 line 188
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC323 line 189
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm323 line 190
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq323 line 192
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA324 line 243
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB324 line 244
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC324 line 245
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm324 line 246
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq324 line 248
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA325 line 299
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB325 line 300
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC325 line 301
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm325 line 302
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq325 line 304
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA326 line 355
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB326 line 356
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC326 line 357
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm326 line 358
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq326 line 360
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA327 line 411
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB327 line 412
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC327 line 413
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm327 line 414
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq327 line 416
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA328 line 467
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB328 line 468
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC328 line 469
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm328 line 470
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq328 line 472
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA329 line 523
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB329 line 524
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC329 line 525
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm329 line 526
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq329 line 528
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA330 line 579
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB330 line 580
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC330 line 581
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm330 line 582
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq330 line 584
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA331 line 773
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB331 line 774
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC331 line 775
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm331 line 776
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq331 line 778
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA332 line 967
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB332 line 968
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC332 line 969
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm332 line 970
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq332 line 972
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA333 line 1161
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB333 line 1162
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC333 line 1163
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm333 line 1164
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq333 line 1166
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA334 line 1217
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB334 line 1218
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC334 line 1219
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm334 line 1220
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq334 line 1222
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA335 line 1273
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB335 line 1274
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC335 line 1275
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm335 line 1276
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq335 line 1278
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA336 line 1329
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB336 line 1330
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC336 line 1331
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm336 line 1332
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq336 line 1334
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA337 line 1385
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB337 line 1386
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC337 line 1387
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm337 line 1388
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq337 line 1390
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA338 line 1441
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB338 line 1442
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC338 line 1443
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm338 line 1444
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq338 line 1446
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA339 line 1497
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB339 line 1498
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC339 line 1499
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm339 line 1500
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq339 line 1502
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA340 line 1553
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB340 line 1554
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC340 line 1555
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm340 line 1556
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq340 line 1558
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA341 line 1747
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB341 line 1748
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC341 line 1749
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm341 line 1750
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq341 line 1752
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA342 line 1941
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB342 line 1942
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC342 line 1943
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm342 line 1944
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq342 line 1946
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA343 line 2135
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB343 line 2136
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC343 line 2137
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm343 line 2138
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq343 line 2140
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA344 line 2191
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB344 line 2192
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC344 line 2193
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm344 line 2194
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq344 line 2196
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA345 line 2247
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB345 line 2248
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC345 line 2249
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm345 line 2250
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq345 line 2252
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA346 line 2303
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB346 line 2304
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC346 line 2305
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm346 line 2306
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq346 line 2308
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA347 line 2359
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB347 line 2360
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC347 line 2361
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm347 line 2362
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq347 line 2364
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA348 line 2415
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB348 line 2416
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC348 line 2417
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm348 line 2418
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq348 line 2420
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA349 line 2471
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB349 line 2472
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC349 line 2473
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm349 line 2474
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq349 line 2476
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA350 line 2527
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB350 line 2528
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC350 line 2529
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm350 line 2530
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq350 line 2532
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA351 line 2583
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB351 line 2584
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC351 line 2585
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm351 line 2586
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq351 line 2588