OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources1.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA32 line 15
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB32 line 16
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC32 line 17
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm32 line 18
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq32 line 20
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA33 line 71
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB33 line 72
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC33 line 73
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm33 line 74
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq33 line 76
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA34 line 127
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB34 line 128
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC34 line 129
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm34 line 130
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq34 line 132
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA35 line 183
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB35 line 184
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC35 line 185
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm35 line 186
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq35 line 188
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA36 line 239
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB36 line 240
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC36 line 241
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm36 line 242
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq36 line 244
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA37 line 295
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB37 line 296
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC37 line 297
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm37 line 298
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq37 line 300
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA38 line 489
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB38 line 490
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC38 line 491
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm38 line 492
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq38 line 494
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA39 line 683
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB39 line 684
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC39 line 685
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm39 line 686
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq39 line 688
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA40 line 877
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB40 line 878
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC40 line 879
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm40 line 880
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq40 line 882
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA41 line 933
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB41 line 934
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC41 line 935
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm41 line 936
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq41 line 938
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA42 line 989
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB42 line 990
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC42 line 991
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm42 line 992
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq42 line 994
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA43 line 1045
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB43 line 1046
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC43 line 1047
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm43 line 1048
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq43 line 1050
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA44 line 1101
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB44 line 1102
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC44 line 1103
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm44 line 1104
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq44 line 1106
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA45 line 1157
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB45 line 1158
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC45 line 1159
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm45 line 1160
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq45 line 1162
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA46 line 1213
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB46 line 1214
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC46 line 1215
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm46 line 1216
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq46 line 1218
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA47 line 1269
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB47 line 1270
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC47 line 1271
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm47 line 1272
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq47 line 1274
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA48 line 1325
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB48 line 1326
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC48 line 1327
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm48 line 1328
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq48 line 1330
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA49 line 1381
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB49 line 1382
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC49 line 1383
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm49 line 1384
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq49 line 1386
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA50 line 1575
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB50 line 1576
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC50 line 1577
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm50 line 1578
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq50 line 1580
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA51 line 1769
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB51 line 1770
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC51 line 1771
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm51 line 1772
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq51 line 1774
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA52 line 1825
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB52 line 1826
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC52 line 1827
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm52 line 1828
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq52 line 1830
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA53 line 1881
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB53 line 1882
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC53 line 1883
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm53 line 1884
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq53 line 1886
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA54 line 1937
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB54 line 1938
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC54 line 1939
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm54 line 1940
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq54 line 1942
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA55 line 1993
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB55 line 1994
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC55 line 1995
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm55 line 1996
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq55 line 1998
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA56 line 2049
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB56 line 2050
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC56 line 2051
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm56 line 2052
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq56 line 2054
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA57 line 2243
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB57 line 2244
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC57 line 2245
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm57 line 2246
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq57 line 2248
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA58 line 2437
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB58 line 2438
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC58 line 2439
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm58 line 2440
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq58 line 2442
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA59 line 2631
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB59 line 2632
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC59 line 2633
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm59 line 2634
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq59 line 2636
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA60 line 2687
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB60 line 2688
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC60 line 2689
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm60 line 2690
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq60 line 2692
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA61 line 2743
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB61 line 2744
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC61 line 2745
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm61 line 2746
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq61 line 2748
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA62 line 2799
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB62 line 2800
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC62 line 2801
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm62 line 2802
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq62 line 2804
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA63 line 2855
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB63 line 2856
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC63 line 2857
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm63 line 2858
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq63 line 2860