OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources81.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA2592 line 64
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB2592 line 65
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC2592 line 66
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2592 line 67
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2592 line 69
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA2593 line 258
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB2593 line 259
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC2593 line 260
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2593 line 261
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2593 line 263
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA2594 line 452
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB2594 line 453
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC2594 line 454
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2594 line 455
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2594 line 457
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA2595 line 646
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB2595 line 647
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC2595 line 648
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2595 line 649
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2595 line 651
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA2596 line 840
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB2596 line 841
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC2596 line 842
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2596 line 843
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2596 line 845
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA2597 line 1034
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB2597 line 1035
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC2597 line 1036
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2597 line 1037
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2597 line 1039
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA2598 line 1228
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB2598 line 1229
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC2598 line 1230
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2598 line 1231
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2598 line 1233
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA2599 line 1422
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB2599 line 1423
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC2599 line 1424
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2599 line 1425
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2599 line 1427
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA2600 line 1616
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB2600 line 1617
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC2600 line 1618
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2600 line 1619
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2600 line 1621
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA2601 line 1810
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB2601 line 1811
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC2601 line 1812
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2601 line 1813
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2601 line 1815
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA2602 line 2004
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB2602 line 2005
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC2602 line 2006
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2602 line 2007
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2602 line 2009
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA2603 line 2198
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB2603 line 2199
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC2603 line 2200
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2603 line 2201
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2603 line 2203
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA2604 line 2392
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB2604 line 2393
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC2604 line 2394
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2604 line 2395
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2604 line 2397
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA2605 line 2586
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB2605 line 2587
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC2605 line 2588
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2605 line 2589
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2605 line 2591
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA2606 line 2780
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB2606 line 2781
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC2606 line 2782
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2606 line 2783
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2606 line 2785
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA2607 line 2974
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB2607 line 2975
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC2607 line 2976
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2607 line 2977
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2607 line 2979
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA2608 line 3168
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB2608 line 3169
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC2608 line 3170
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2608 line 3171
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2608 line 3173
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA2609 line 3362
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB2609 line 3363
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC2609 line 3364
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2609 line 3365
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2609 line 3367
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA2610 line 3556
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB2610 line 3557
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC2610 line 3558
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2610 line 3559
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2610 line 3561
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA2611 line 3750
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB2611 line 3751
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC2611 line 3752
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2611 line 3753
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2611 line 3755
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA2612 line 3944
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB2612 line 3945
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC2612 line 3946
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2612 line 3947
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2612 line 3949
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA2613 line 4138
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB2613 line 4139
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC2613 line 4140
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2613 line 4141
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2613 line 4143
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA2614 line 4332
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB2614 line 4333
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC2614 line 4334
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2614 line 4335
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2614 line 4337
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA2615 line 4526
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB2615 line 4527
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC2615 line 4528
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2615 line 4529
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2615 line 4531
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA2616 line 4720
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB2616 line 4721
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC2616 line 4722
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2616 line 4723
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2616 line 4725
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA2617 line 4914
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB2617 line 4915
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC2617 line 4916
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2617 line 4917
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2617 line 4919
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA2618 line 5108
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB2618 line 5109
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC2618 line 5110
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2618 line 5111
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2618 line 5113
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA2619 line 5302
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB2619 line 5303
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC2619 line 5304
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2619 line 5305
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2619 line 5307
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA2620 line 5496
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB2620 line 5497
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC2620 line 5498
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2620 line 5499
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2620 line 5501
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA2621 line 5690
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB2621 line 5691
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC2621 line 5692
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2621 line 5693
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2621 line 5695
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA2622 line 5884
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB2622 line 5885
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC2622 line 5886
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2622 line 5887
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2622 line 5889
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA2623 line 6078
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB2623 line 6079
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC2623 line 6080
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2623 line 6081
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2623 line 6083