OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources3.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA96 line 20
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB96 line 21
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC96 line 22
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm96 line 23
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq96 line 25
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA97 line 76
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB97 line 77
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC97 line 78
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm97 line 79
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq97 line 81
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA98 line 132
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB98 line 133
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC98 line 134
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm98 line 135
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq98 line 137
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA99 line 188
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB99 line 189
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC99 line 190
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm99 line 191
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq99 line 193
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA100 line 244
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB100 line 245
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC100 line 246
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm100 line 247
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq100 line 249
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA101 line 300
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB101 line 301
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC101 line 302
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm101 line 303
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq101 line 305
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA102 line 356
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB102 line 357
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC102 line 358
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm102 line 359
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq102 line 361
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA103 line 412
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB103 line 413
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC103 line 414
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm103 line 415
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq103 line 417
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA104 line 468
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB104 line 469
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC104 line 470
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm104 line 471
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq104 line 473
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA105 line 662
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB105 line 663
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC105 line 664
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm105 line 665
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq105 line 667
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA106 line 856
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB106 line 857
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC106 line 858
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm106 line 859
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq106 line 861
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA107 line 912
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB107 line 913
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC107 line 914
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm107 line 915
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq107 line 917
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA108 line 968
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB108 line 969
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC108 line 970
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm108 line 971
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq108 line 973
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA109 line 1024
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB109 line 1025
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC109 line 1026
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm109 line 1027
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq109 line 1029
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA110 line 1080
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB110 line 1081
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC110 line 1082
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm110 line 1083
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq110 line 1085
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA111 line 1136
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB111 line 1137
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC111 line 1138
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm111 line 1139
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq111 line 1141
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA112 line 1330
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB112 line 1331
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC112 line 1332
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm112 line 1333
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq112 line 1335
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA113 line 1524
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB113 line 1525
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC113 line 1526
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm113 line 1527
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq113 line 1529
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA114 line 1718
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB114 line 1719
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC114 line 1720
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm114 line 1721
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq114 line 1723
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA115 line 1912
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB115 line 1913
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC115 line 1914
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm115 line 1915
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq115 line 1917
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA116 line 1968
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB116 line 1969
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC116 line 1970
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm116 line 1971
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq116 line 1973
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA117 line 2024
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB117 line 2025
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC117 line 2026
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm117 line 2027
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq117 line 2029
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA118 line 2218
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB118 line 2219
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC118 line 2220
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm118 line 2221
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq118 line 2223
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA119 line 2412
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB119 line 2413
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC119 line 2414
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm119 line 2415
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq119 line 2417
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA120 line 2606
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB120 line 2607
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC120 line 2608
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm120 line 2609
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq120 line 2611
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA121 line 2800
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB121 line 2801
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC121 line 2802
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm121 line 2803
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq121 line 2805
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA122 line 2994
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB122 line 2995
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC122 line 2996
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm122 line 2997
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq122 line 2999
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA123 line 3050
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB123 line 3051
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC123 line 3052
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm123 line 3053
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq123 line 3055
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA124 line 3106
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB124 line 3107
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC124 line 3108
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm124 line 3109
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq124 line 3111
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA125 line 3162
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB125 line 3163
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC125 line 3164
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm125 line 3165
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq125 line 3167
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA126 line 3218
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB126 line 3219
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC126 line 3220
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm126 line 3221
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq126 line 3223
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA127 line 3274
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB127 line 3275
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC127 line 3276
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm127 line 3277
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq127 line 3279