OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources33.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA1056 line 35
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB1056 line 36
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC1056 line 37
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1056 line 38
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1056 line 40
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA1057 line 229
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB1057 line 230
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC1057 line 231
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1057 line 232
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1057 line 234
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA1058 line 423
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB1058 line 424
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC1058 line 425
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1058 line 426
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1058 line 428
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA1059 line 617
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB1059 line 618
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC1059 line 619
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1059 line 620
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1059 line 622
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA1060 line 811
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB1060 line 812
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC1060 line 813
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1060 line 814
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1060 line 816
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA1061 line 1005
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB1061 line 1006
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC1061 line 1007
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1061 line 1008
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1061 line 1010
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA1062 line 1199
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB1062 line 1200
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC1062 line 1201
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1062 line 1202
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1062 line 1204
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA1063 line 1393
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB1063 line 1394
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC1063 line 1395
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1063 line 1396
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1063 line 1398
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA1064 line 1587
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB1064 line 1588
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC1064 line 1589
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1064 line 1590
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1064 line 1592
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA1065 line 1781
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB1065 line 1782
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC1065 line 1783
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1065 line 1784
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1065 line 1786
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA1066 line 1975
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB1066 line 1976
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC1066 line 1977
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1066 line 1978
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1066 line 1980
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA1067 line 2169
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB1067 line 2170
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC1067 line 2171
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1067 line 2172
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1067 line 2174
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA1068 line 2363
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB1068 line 2364
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC1068 line 2365
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1068 line 2366
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1068 line 2368
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA1069 line 2557
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB1069 line 2558
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC1069 line 2559
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1069 line 2560
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1069 line 2562
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA1070 line 2751
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB1070 line 2752
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC1070 line 2753
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1070 line 2754
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1070 line 2756
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA1071 line 2945
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB1071 line 2946
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC1071 line 2947
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1071 line 2948
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1071 line 2950
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA1072 line 3139
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB1072 line 3140
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC1072 line 3141
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1072 line 3142
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1072 line 3144
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA1073 line 3333
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB1073 line 3334
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC1073 line 3335
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1073 line 3336
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1073 line 3338
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA1074 line 3527
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB1074 line 3528
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC1074 line 3529
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1074 line 3530
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1074 line 3532
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA1075 line 3721
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB1075 line 3722
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC1075 line 3723
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1075 line 3724
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1075 line 3726
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA1076 line 3915
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB1076 line 3916
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC1076 line 3917
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1076 line 3918
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1076 line 3920
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA1077 line 4109
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB1077 line 4110
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC1077 line 4111
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1077 line 4112
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1077 line 4114
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA1078 line 4303
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB1078 line 4304
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC1078 line 4305
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1078 line 4306
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1078 line 4308
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA1079 line 4497
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB1079 line 4498
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC1079 line 4499
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1079 line 4500
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1079 line 4502
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA1080 line 4691
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB1080 line 4692
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC1080 line 4693
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1080 line 4694
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1080 line 4696
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA1081 line 4885
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB1081 line 4886
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC1081 line 4887
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1081 line 4888
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1081 line 4890
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA1082 line 5079
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB1082 line 5080
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC1082 line 5081
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1082 line 5082
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1082 line 5084
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA1083 line 5273
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB1083 line 5274
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC1083 line 5275
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1083 line 5276
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1083 line 5278
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA1084 line 5467
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB1084 line 5468
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC1084 line 5469
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1084 line 5470
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1084 line 5472
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA1085 line 5661
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB1085 line 5662
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC1085 line 5663
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1085 line 5664
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1085 line 5666
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA1086 line 5855
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB1086 line 5856
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC1086 line 5857
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1086 line 5858
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1086 line 5860
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA1087 line 6049
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB1087 line 6050
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC1087 line 6051
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1087 line 6052
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1087 line 6054