OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources6.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA192 line 15
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB192 line 16
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC192 line 17
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm192 line 18
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq192 line 20
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA193 line 71
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB193 line 72
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC193 line 73
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm193 line 74
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq193 line 76
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA194 line 127
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB194 line 128
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC194 line 129
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm194 line 130
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq194 line 132
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA195 line 321
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB195 line 322
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC195 line 323
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm195 line 324
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq195 line 326
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA196 line 515
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB196 line 516
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC196 line 517
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm196 line 518
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq196 line 520
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA197 line 709
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB197 line 710
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC197 line 711
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm197 line 712
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq197 line 714
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA198 line 765
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB198 line 766
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC198 line 767
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm198 line 768
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq198 line 770
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA199 line 821
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB199 line 822
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC199 line 823
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm199 line 824
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq199 line 826
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA200 line 877
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB200 line 878
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC200 line 879
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm200 line 880
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq200 line 882
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA201 line 933
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB201 line 934
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC201 line 935
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm201 line 936
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq201 line 938
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA202 line 989
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB202 line 990
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC202 line 991
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm202 line 992
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq202 line 994
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA203 line 1183
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB203 line 1184
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC203 line 1185
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm203 line 1186
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq203 line 1188
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA204 line 1377
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB204 line 1378
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC204 line 1379
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm204 line 1380
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq204 line 1382
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA205 line 1571
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB205 line 1572
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC205 line 1573
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm205 line 1574
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq205 line 1576
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA206 line 1627
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB206 line 1628
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC206 line 1629
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm206 line 1630
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq206 line 1632
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA207 line 1683
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB207 line 1684
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC207 line 1685
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm207 line 1686
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq207 line 1688
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA208 line 1739
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB208 line 1740
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC208 line 1741
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm208 line 1742
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq208 line 1744
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA209 line 1795
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB209 line 1796
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC209 line 1797
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm209 line 1798
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq209 line 1800
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA210 line 1851
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB210 line 1852
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC210 line 1853
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm210 line 1854
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq210 line 1856
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA211 line 1907
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB211 line 1908
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC211 line 1909
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm211 line 1910
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq211 line 1912
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA212 line 1963
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB212 line 1964
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC212 line 1965
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm212 line 1966
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq212 line 1968
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA213 line 2157
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB213 line 2158
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC213 line 2159
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm213 line 2160
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq213 line 2162
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA214 line 2351
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB214 line 2352
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC214 line 2353
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm214 line 2354
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq214 line 2356
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA215 line 2545
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB215 line 2546
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC215 line 2547
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm215 line 2548
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq215 line 2550
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA216 line 2601
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB216 line 2602
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC216 line 2603
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm216 line 2604
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq216 line 2606
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA217 line 2657
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB217 line 2658
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC217 line 2659
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm217 line 2660
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq217 line 2662
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA218 line 2713
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB218 line 2714
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC218 line 2715
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm218 line 2716
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq218 line 2718
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA219 line 2769
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB219 line 2770
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC219 line 2771
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm219 line 2772
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq219 line 2774
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA220 line 2825
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB220 line 2826
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC220 line 2827
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm220 line 2828
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq220 line 2830
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA221 line 3019
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB221 line 3020
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC221 line 3021
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm221 line 3022
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq221 line 3024
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA222 line 3213
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB222 line 3214
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC222 line 3215
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm222 line 3216
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq222 line 3218
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA223 line 3407
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB223 line 3408
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC223 line 3409
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm223 line 3410
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq223 line 3412