OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources11.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA352 line 21
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB352 line 22
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC352 line 23
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm352 line 24
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq352 line 26
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA353 line 215
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB353 line 216
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC353 line 217
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm353 line 218
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq353 line 220
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA354 line 409
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB354 line 410
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC354 line 411
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm354 line 412
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq354 line 414
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA355 line 465
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB355 line 466
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC355 line 467
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm355 line 468
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq355 line 470
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA356 line 521
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB356 line 522
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC356 line 523
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm356 line 524
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq356 line 526
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA357 line 577
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB357 line 578
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC357 line 579
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm357 line 580
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq357 line 582
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA358 line 633
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB358 line 634
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC358 line 635
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm358 line 636
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq358 line 638
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA359 line 689
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB359 line 690
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC359 line 691
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm359 line 692
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq359 line 694
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA360 line 883
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB360 line 884
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC360 line 885
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm360 line 886
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq360 line 888
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA361 line 1077
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB361 line 1078
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC361 line 1079
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm361 line 1080
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq361 line 1082
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA362 line 1271
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB362 line 1272
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC362 line 1273
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm362 line 1274
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq362 line 1276
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA363 line 1327
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB363 line 1328
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC363 line 1329
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm363 line 1330
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq363 line 1332
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA364 line 1383
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB364 line 1384
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC364 line 1385
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm364 line 1386
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq364 line 1388
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA365 line 1439
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB365 line 1440
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC365 line 1441
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm365 line 1442
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq365 line 1444
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA366 line 1495
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB366 line 1496
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC366 line 1497
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm366 line 1498
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq366 line 1500
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA367 line 1551
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB367 line 1552
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC367 line 1553
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm367 line 1554
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq367 line 1556
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA368 line 1607
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB368 line 1608
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC368 line 1609
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm368 line 1610
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq368 line 1612
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA369 line 1663
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB369 line 1664
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC369 line 1665
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm369 line 1666
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq369 line 1668
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA370 line 1857
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB370 line 1858
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC370 line 1859
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm370 line 1860
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq370 line 1862
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA371 line 2051
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB371 line 2052
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC371 line 2053
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm371 line 2054
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq371 line 2056
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA372 line 2245
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB372 line 2246
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC372 line 2247
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm372 line 2248
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq372 line 2250
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA373 line 2301
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB373 line 2302
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC373 line 2303
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm373 line 2304
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq373 line 2306
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA374 line 2357
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB374 line 2358
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC374 line 2359
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm374 line 2360
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq374 line 2362
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA375 line 2413
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB375 line 2414
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC375 line 2415
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm375 line 2416
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq375 line 2418
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA376 line 2469
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB376 line 2470
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC376 line 2471
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm376 line 2472
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq376 line 2474
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA377 line 2525
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB377 line 2526
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC377 line 2527
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm377 line 2528
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq377 line 2530
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA378 line 2581
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB378 line 2582
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC378 line 2583
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm378 line 2584
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq378 line 2586
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA379 line 2637
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB379 line 2638
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC379 line 2639
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm379 line 2640
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq379 line 2642
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA380 line 2831
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB380 line 2832
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC380 line 2833
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm380 line 2834
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq380 line 2836
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA381 line 3025
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB381 line 3026
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC381 line 3027
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm381 line 3028
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq381 line 3030
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA382 line 3219
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB382 line 3220
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC382 line 3221
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm382 line 3222
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq382 line 3224
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA383 line 3275
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB383 line 3276
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC383 line 3277
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm383 line 3278
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq383 line 3280