OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources66.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA2112 line 37
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB2112 line 38
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC2112 line 39
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2112 line 40
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2112 line 42
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA2113 line 93
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB2113 line 94
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC2113 line 95
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2113 line 96
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2113 line 98
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA2114 line 149
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB2114 line 150
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC2114 line 151
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2114 line 152
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2114 line 154
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA2115 line 205
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB2115 line 206
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC2115 line 207
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2115 line 208
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2115 line 210
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA2116 line 261
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB2116 line 262
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC2116 line 263
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2116 line 264
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2116 line 266
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA2117 line 317
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB2117 line 318
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC2117 line 319
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2117 line 320
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2117 line 322
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA2118 line 373
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB2118 line 374
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC2118 line 375
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2118 line 376
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2118 line 378
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA2119 line 429
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB2119 line 430
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC2119 line 431
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2119 line 432
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2119 line 434
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA2120 line 485
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB2120 line 486
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC2120 line 487
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2120 line 488
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2120 line 490
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA2121 line 541
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB2121 line 542
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC2121 line 543
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2121 line 544
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2121 line 546
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA2122 line 597
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB2122 line 598
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC2122 line 599
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2122 line 600
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2122 line 602
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA2123 line 653
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB2123 line 654
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC2123 line 655
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2123 line 656
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2123 line 658
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA2124 line 709
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB2124 line 710
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC2124 line 711
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2124 line 712
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2124 line 714
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA2125 line 765
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB2125 line 766
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC2125 line 767
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2125 line 768
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2125 line 770
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA2126 line 821
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB2126 line 822
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC2126 line 823
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2126 line 824
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2126 line 826
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA2127 line 877
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB2127 line 878
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC2127 line 879
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2127 line 880
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2127 line 882
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA2128 line 933
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB2128 line 934
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC2128 line 935
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2128 line 936
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2128 line 938
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA2129 line 989
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB2129 line 990
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC2129 line 991
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2129 line 992
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2129 line 994
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA2130 line 1045
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB2130 line 1046
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC2130 line 1047
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2130 line 1048
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2130 line 1050
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA2131 line 1101
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB2131 line 1102
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC2131 line 1103
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2131 line 1104
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2131 line 1106
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA2132 line 1157
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB2132 line 1158
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC2132 line 1159
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2132 line 1160
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2132 line 1162
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA2133 line 1213
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB2133 line 1214
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC2133 line 1215
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2133 line 1216
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2133 line 1218
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA2134 line 1269
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB2134 line 1270
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC2134 line 1271
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2134 line 1272
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2134 line 1274
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA2135 line 1325
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB2135 line 1326
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC2135 line 1327
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2135 line 1328
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2135 line 1330
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA2136 line 1519
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB2136 line 1520
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC2136 line 1521
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2136 line 1522
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2136 line 1524
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA2137 line 1713
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB2137 line 1714
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC2137 line 1715
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2137 line 1716
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2137 line 1718
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA2138 line 1907
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB2138 line 1908
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC2138 line 1909
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2138 line 1910
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2138 line 1912
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA2139 line 2101
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB2139 line 2102
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC2139 line 2103
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2139 line 2104
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2139 line 2106
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA2140 line 2295
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB2140 line 2296
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC2140 line 2297
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2140 line 2298
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2140 line 2300
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA2141 line 2489
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB2141 line 2490
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC2141 line 2491
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2141 line 2492
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2141 line 2494
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA2142 line 2683
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB2142 line 2684
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC2142 line 2685
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2142 line 2686
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2142 line 2688
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA2143 line 2877
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB2143 line 2878
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC2143 line 2879
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2143 line 2880
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2143 line 2882