OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources4.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA128 line 24
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB128 line 25
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC128 line 26
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm128 line 27
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq128 line 29
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA129 line 80
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB129 line 81
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC129 line 82
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm129 line 83
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq129 line 85
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA130 line 274
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB130 line 275
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC130 line 276
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm130 line 277
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq130 line 279
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA131 line 468
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB131 line 469
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC131 line 470
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm131 line 471
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq131 line 473
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA132 line 662
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB132 line 663
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC132 line 664
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm132 line 665
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq132 line 667
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA133 line 718
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB133 line 719
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC133 line 720
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm133 line 721
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq133 line 723
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA134 line 912
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB134 line 913
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC134 line 914
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm134 line 915
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq134 line 917
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA135 line 1106
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB135 line 1107
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC135 line 1108
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm135 line 1109
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq135 line 1111
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA136 line 1300
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB136 line 1301
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC136 line 1302
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm136 line 1303
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq136 line 1305
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA137 line 1494
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB137 line 1495
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC137 line 1496
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm137 line 1497
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq137 line 1499
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA138 line 1688
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB138 line 1689
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC138 line 1690
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm138 line 1691
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq138 line 1693
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA139 line 1744
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB139 line 1745
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC139 line 1746
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm139 line 1747
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq139 line 1749
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA140 line 1800
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB140 line 1801
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC140 line 1802
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm140 line 1803
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq140 line 1805
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA141 line 1856
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB141 line 1857
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC141 line 1858
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm141 line 1859
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq141 line 1861
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA142 line 1912
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB142 line 1913
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC142 line 1914
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm142 line 1915
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq142 line 1917
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA143 line 1968
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB143 line 1969
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC143 line 1970
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm143 line 1971
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq143 line 1973
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA144 line 2024
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB144 line 2025
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC144 line 2026
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm144 line 2027
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq144 line 2029
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA145 line 2080
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB145 line 2081
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC145 line 2082
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm145 line 2083
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq145 line 2085
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA146 line 2274
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB146 line 2275
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC146 line 2276
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm146 line 2277
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq146 line 2279
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA147 line 2468
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB147 line 2469
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC147 line 2470
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm147 line 2471
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq147 line 2473
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA148 line 2662
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB148 line 2663
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC148 line 2664
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm148 line 2665
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq148 line 2667
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA149 line 2718
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB149 line 2719
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC149 line 2720
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm149 line 2721
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq149 line 2723
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA150 line 2912
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB150 line 2913
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC150 line 2914
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm150 line 2915
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq150 line 2917
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA151 line 3106
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB151 line 3107
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC151 line 3108
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm151 line 3109
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq151 line 3111
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA152 line 3300
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB152 line 3301
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC152 line 3302
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm152 line 3303
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq152 line 3305
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA153 line 3356
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB153 line 3357
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC153 line 3358
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm153 line 3359
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq153 line 3361
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA154 line 3412
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB154 line 3413
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC154 line 3414
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm154 line 3415
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq154 line 3417
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA155 line 3468
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB155 line 3469
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC155 line 3470
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm155 line 3471
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq155 line 3473
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA156 line 3524
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB156 line 3525
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC156 line 3526
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm156 line 3527
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq156 line 3529
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA157 line 3580
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB157 line 3581
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC157 line 3582
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm157 line 3583
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq157 line 3585
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA158 line 3774
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB158 line 3775
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC158 line 3776
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm158 line 3777
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq158 line 3779
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA159 line 3968
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB159 line 3969
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC159 line 3970
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm159 line 3971
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq159 line 3973