OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources34.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA1088 line 42
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB1088 line 43
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC1088 line 44
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1088 line 45
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1088 line 47
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA1089 line 236
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB1089 line 237
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC1089 line 238
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1089 line 239
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1089 line 241
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA1090 line 430
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB1090 line 431
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC1090 line 432
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1090 line 433
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1090 line 435
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA1091 line 624
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB1091 line 625
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC1091 line 626
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1091 line 627
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1091 line 629
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA1092 line 818
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB1092 line 819
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC1092 line 820
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1092 line 821
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1092 line 823
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA1093 line 1012
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB1093 line 1013
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC1093 line 1014
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1093 line 1015
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1093 line 1017
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA1094 line 1206
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB1094 line 1207
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC1094 line 1208
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1094 line 1209
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1094 line 1211
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA1095 line 1400
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB1095 line 1401
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC1095 line 1402
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1095 line 1403
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1095 line 1405
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA1096 line 1594
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB1096 line 1595
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC1096 line 1596
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1096 line 1597
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1096 line 1599
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA1097 line 1788
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB1097 line 1789
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC1097 line 1790
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1097 line 1791
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1097 line 1793
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA1098 line 1982
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB1098 line 1983
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC1098 line 1984
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1098 line 1985
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1098 line 1987
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA1099 line 2176
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB1099 line 2177
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC1099 line 2178
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1099 line 2179
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1099 line 2181
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA1100 line 2370
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB1100 line 2371
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC1100 line 2372
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1100 line 2373
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1100 line 2375
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA1101 line 2564
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB1101 line 2565
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC1101 line 2566
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1101 line 2567
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1101 line 2569
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA1102 line 2758
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB1102 line 2759
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC1102 line 2760
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1102 line 2761
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1102 line 2763
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA1103 line 2952
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB1103 line 2953
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC1103 line 2954
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1103 line 2955
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1103 line 2957
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA1104 line 3146
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB1104 line 3147
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC1104 line 3148
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1104 line 3149
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1104 line 3151
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA1105 line 3340
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB1105 line 3341
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC1105 line 3342
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1105 line 3343
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1105 line 3345
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA1106 line 3534
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB1106 line 3535
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC1106 line 3536
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1106 line 3537
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1106 line 3539
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA1107 line 3728
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB1107 line 3729
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC1107 line 3730
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1107 line 3731
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1107 line 3733
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA1108 line 3922
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB1108 line 3923
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC1108 line 3924
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1108 line 3925
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1108 line 3927
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA1109 line 4116
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB1109 line 4117
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC1109 line 4118
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1109 line 4119
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1109 line 4121
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA1110 line 4310
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB1110 line 4311
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC1110 line 4312
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1110 line 4313
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1110 line 4315
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA1111 line 4504
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB1111 line 4505
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC1111 line 4506
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1111 line 4507
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1111 line 4509
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA1112 line 4698
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB1112 line 4699
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC1112 line 4700
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1112 line 4701
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1112 line 4703
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA1113 line 4892
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB1113 line 4893
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC1113 line 4894
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1113 line 4895
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1113 line 4897
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA1114 line 5086
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB1114 line 5087
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC1114 line 5088
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1114 line 5089
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1114 line 5091
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA1115 line 5280
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB1115 line 5281
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC1115 line 5282
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1115 line 5283
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1115 line 5285
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA1116 line 5336
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB1116 line 5337
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC1116 line 5338
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1116 line 5339
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1116 line 5341
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA1117 line 5530
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB1117 line 5531
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC1117 line 5532
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1117 line 5533
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1117 line 5535
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA1118 line 5724
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB1118 line 5725
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC1118 line 5726
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1118 line 5727
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1118 line 5729
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA1119 line 5918
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB1119 line 5919
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC1119 line 5920
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1119 line 5921
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1119 line 5923