OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources18.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA576 line 23
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB576 line 24
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC576 line 25
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm576 line 26
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq576 line 28
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA577 line 217
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB577 line 218
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC577 line 219
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm577 line 220
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq577 line 222
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA578 line 273
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB578 line 274
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC578 line 275
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm578 line 276
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq578 line 278
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA579 line 467
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB579 line 468
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC579 line 469
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm579 line 470
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq579 line 472
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA580 line 661
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB580 line 662
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC580 line 663
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm580 line 664
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq580 line 666
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA581 line 855
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB581 line 856
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC581 line 857
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm581 line 858
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq581 line 860
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA582 line 911
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB582 line 912
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC582 line 913
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm582 line 914
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq582 line 916
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA583 line 967
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB583 line 968
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC583 line 969
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm583 line 970
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq583 line 972
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA584 line 1023
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB584 line 1024
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC584 line 1025
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm584 line 1026
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq584 line 1028
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA585 line 1079
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB585 line 1080
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC585 line 1081
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm585 line 1082
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq585 line 1084
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA586 line 1135
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB586 line 1136
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC586 line 1137
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm586 line 1138
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq586 line 1140
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA587 line 1191
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB587 line 1192
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC587 line 1193
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm587 line 1194
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq587 line 1196
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA588 line 1247
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB588 line 1248
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC588 line 1249
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm588 line 1250
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq588 line 1252
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA589 line 1441
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB589 line 1442
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC589 line 1443
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm589 line 1444
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq589 line 1446
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA590 line 1635
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB590 line 1636
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC590 line 1637
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm590 line 1638
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq590 line 1640
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA591 line 1829
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB591 line 1830
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC591 line 1831
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm591 line 1832
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq591 line 1834
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA592 line 2023
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB592 line 2024
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC592 line 2025
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm592 line 2026
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq592 line 2028
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA593 line 2217
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB593 line 2218
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC593 line 2219
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm593 line 2220
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq593 line 2222
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA594 line 2273
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB594 line 2274
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC594 line 2275
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm594 line 2276
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq594 line 2278
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA595 line 2467
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB595 line 2468
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC595 line 2469
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm595 line 2470
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq595 line 2472
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA596 line 2661
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB596 line 2662
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC596 line 2663
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm596 line 2664
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq596 line 2666
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA597 line 2855
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB597 line 2856
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC597 line 2857
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm597 line 2858
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq597 line 2860
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA598 line 2911
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB598 line 2912
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC598 line 2913
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm598 line 2914
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq598 line 2916
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA599 line 2967
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB599 line 2968
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC599 line 2969
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm599 line 2970
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq599 line 2972
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA600 line 3023
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB600 line 3024
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC600 line 3025
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm600 line 3026
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq600 line 3028
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA601 line 3079
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB601 line 3080
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC601 line 3081
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm601 line 3082
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq601 line 3084
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA602 line 3135
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB602 line 3136
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC602 line 3137
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm602 line 3138
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq602 line 3140
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA603 line 3191
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB603 line 3192
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC603 line 3193
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm603 line 3194
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq603 line 3196
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA604 line 3385
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB604 line 3386
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC604 line 3387
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm604 line 3388
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq604 line 3390
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA605 line 3579
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB605 line 3580
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC605 line 3581
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm605 line 3582
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq605 line 3584
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA606 line 3773
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB606 line 3774
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC606 line 3775
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm606 line 3776
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq606 line 3778
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA607 line 3967
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB607 line 3968
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC607 line 3969
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm607 line 3970
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq607 line 3972