OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources63.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA2016 line 39
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB2016 line 40
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC2016 line 41
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2016 line 42
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2016 line 44
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA2017 line 95
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB2017 line 96
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC2017 line 97
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2017 line 98
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2017 line 100
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA2018 line 151
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB2018 line 152
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC2018 line 153
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2018 line 154
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2018 line 156
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA2019 line 207
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB2019 line 208
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC2019 line 209
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2019 line 210
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2019 line 212
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA2020 line 263
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB2020 line 264
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC2020 line 265
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2020 line 266
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2020 line 268
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA2021 line 319
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB2021 line 320
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC2021 line 321
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2021 line 322
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2021 line 324
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA2022 line 513
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB2022 line 514
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC2022 line 515
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2022 line 516
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2022 line 518
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA2023 line 707
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB2023 line 708
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC2023 line 709
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2023 line 710
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2023 line 712
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA2024 line 901
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB2024 line 902
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC2024 line 903
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2024 line 904
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2024 line 906
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA2025 line 957
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB2025 line 958
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC2025 line 959
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2025 line 960
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2025 line 962
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA2026 line 1013
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB2026 line 1014
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC2026 line 1015
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2026 line 1016
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2026 line 1018
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA2027 line 1069
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB2027 line 1070
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC2027 line 1071
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2027 line 1072
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2027 line 1074
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA2028 line 1263
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB2028 line 1264
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC2028 line 1265
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2028 line 1266
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2028 line 1268
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA2029 line 1457
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB2029 line 1458
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC2029 line 1459
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2029 line 1460
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2029 line 1462
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA2030 line 1651
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB2030 line 1652
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC2030 line 1653
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2030 line 1654
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2030 line 1656
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA2031 line 1845
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB2031 line 1846
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC2031 line 1847
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2031 line 1848
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2031 line 1850
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA2032 line 2039
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB2032 line 2040
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC2032 line 2041
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2032 line 2042
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2032 line 2044
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA2033 line 2233
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB2033 line 2234
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC2033 line 2235
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2033 line 2236
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2033 line 2238
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA2034 line 2289
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB2034 line 2290
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC2034 line 2291
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2034 line 2292
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2034 line 2294
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA2035 line 2345
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB2035 line 2346
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC2035 line 2347
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2035 line 2348
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2035 line 2350
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA2036 line 2401
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB2036 line 2402
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC2036 line 2403
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2036 line 2404
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2036 line 2406
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA2037 line 2595
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB2037 line 2596
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC2037 line 2597
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2037 line 2598
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2037 line 2600
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA2038 line 2789
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB2038 line 2790
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC2038 line 2791
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2038 line 2792
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2038 line 2794
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA2039 line 2983
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB2039 line 2984
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC2039 line 2985
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2039 line 2986
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2039 line 2988
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA2040 line 3177
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB2040 line 3178
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC2040 line 3179
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2040 line 3180
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2040 line 3182
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA2041 line 3371
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB2041 line 3372
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC2041 line 3373
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2041 line 3374
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2041 line 3376
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA2042 line 3565
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB2042 line 3566
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC2042 line 3567
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2042 line 3568
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2042 line 3570
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA2043 line 3621
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB2043 line 3622
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC2043 line 3623
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2043 line 3624
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2043 line 3626
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA2044 line 3677
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB2044 line 3678
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC2044 line 3679
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2044 line 3680
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2044 line 3682
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA2045 line 3733
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB2045 line 3734
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC2045 line 3735
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2045 line 3736
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2045 line 3738
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA2046 line 3789
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB2046 line 3790
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC2046 line 3791
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2046 line 3792
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2046 line 3794
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA2047 line 3983
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB2047 line 3984
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC2047 line 3985
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2047 line 3986
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2047 line 3988