OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources5.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA160 line 22
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB160 line 23
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC160 line 24
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm160 line 25
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq160 line 27
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA161 line 216
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB161 line 217
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC161 line 218
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm161 line 219
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq161 line 221
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA162 line 410
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB162 line 411
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC162 line 412
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm162 line 413
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq162 line 415
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA163 line 466
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB163 line 467
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC163 line 468
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm163 line 469
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq163 line 471
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA164 line 660
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB164 line 661
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC164 line 662
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm164 line 663
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq164 line 665
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA165 line 854
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB165 line 855
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC165 line 856
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm165 line 857
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq165 line 859
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA166 line 1048
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB166 line 1049
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC166 line 1050
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm166 line 1051
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq166 line 1053
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA167 line 1242
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB167 line 1243
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC167 line 1244
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm167 line 1245
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq167 line 1247
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA168 line 1298
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB168 line 1299
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC168 line 1300
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm168 line 1301
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq168 line 1303
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA169 line 1354
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB169 line 1355
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC169 line 1356
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm169 line 1357
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq169 line 1359
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA170 line 1410
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB170 line 1411
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC170 line 1412
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm170 line 1413
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq170 line 1415
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA171 line 1466
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB171 line 1467
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC171 line 1468
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm171 line 1469
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq171 line 1471
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA172 line 1660
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB172 line 1661
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC172 line 1662
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm172 line 1663
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq172 line 1665
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA173 line 1854
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB173 line 1855
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC173 line 1856
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm173 line 1857
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq173 line 1859
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA174 line 2048
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB174 line 2049
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC174 line 2050
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm174 line 2051
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq174 line 2053
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA175 line 2242
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB175 line 2243
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC175 line 2244
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm175 line 2245
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq175 line 2247
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA176 line 2436
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB176 line 2437
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC176 line 2438
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm176 line 2439
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq176 line 2441
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA177 line 2492
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB177 line 2493
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC177 line 2494
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm177 line 2495
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq177 line 2497
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA178 line 2548
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB178 line 2549
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC178 line 2550
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm178 line 2551
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq178 line 2553
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA179 line 2604
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB179 line 2605
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC179 line 2606
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm179 line 2607
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq179 line 2609
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA180 line 2660
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB180 line 2661
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC180 line 2662
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm180 line 2663
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq180 line 2665
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA181 line 2716
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB181 line 2717
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC181 line 2718
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm181 line 2719
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq181 line 2721
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA182 line 2772
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB182 line 2773
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC182 line 2774
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm182 line 2775
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq182 line 2777
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA183 line 2828
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB183 line 2829
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC183 line 2830
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm183 line 2831
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq183 line 2833
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA184 line 2884
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB184 line 2885
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC184 line 2886
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm184 line 2887
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq184 line 2889
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA185 line 2940
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB185 line 2941
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC185 line 2942
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm185 line 2943
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq185 line 2945
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA186 line 3134
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB186 line 3135
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC186 line 3136
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm186 line 3137
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq186 line 3139
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA187 line 3328
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB187 line 3329
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC187 line 3330
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm187 line 3331
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq187 line 3333
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA188 line 3384
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB188 line 3385
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC188 line 3386
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm188 line 3387
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq188 line 3389
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA189 line 3440
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB189 line 3441
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC189 line 3442
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm189 line 3443
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq189 line 3445
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA190 line 3496
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB190 line 3497
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC190 line 3498
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm190 line 3499
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq190 line 3501
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA191 line 3552
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB191 line 3553
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC191 line 3554
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm191 line 3555
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq191 line 3557