OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources82.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA2624 line 66
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB2624 line 67
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC2624 line 68
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2624 line 69
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2624 line 71
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA2625 line 260
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB2625 line 261
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC2625 line 262
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2625 line 263
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2625 line 265
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA2626 line 454
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB2626 line 455
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC2626 line 456
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2626 line 457
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2626 line 459
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA2627 line 648
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB2627 line 649
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC2627 line 650
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2627 line 651
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2627 line 653
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA2628 line 842
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB2628 line 843
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC2628 line 844
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2628 line 845
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2628 line 847
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA2629 line 1036
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB2629 line 1037
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC2629 line 1038
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2629 line 1039
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2629 line 1041
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA2630 line 1230
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB2630 line 1231
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC2630 line 1232
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2630 line 1233
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2630 line 1235
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA2631 line 1424
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB2631 line 1425
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC2631 line 1426
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2631 line 1427
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2631 line 1429
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA2632 line 1618
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB2632 line 1619
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC2632 line 1620
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2632 line 1621
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2632 line 1623
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA2633 line 1812
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB2633 line 1813
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC2633 line 1814
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2633 line 1815
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2633 line 1817
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA2634 line 2006
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB2634 line 2007
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC2634 line 2008
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2634 line 2009
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2634 line 2011
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA2635 line 2200
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB2635 line 2201
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC2635 line 2202
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2635 line 2203
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2635 line 2205
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA2636 line 2394
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB2636 line 2395
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC2636 line 2396
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2636 line 2397
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2636 line 2399
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA2637 line 2588
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB2637 line 2589
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC2637 line 2590
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2637 line 2591
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2637 line 2593
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA2638 line 2782
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB2638 line 2783
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC2638 line 2784
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2638 line 2785
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2638 line 2787
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA2639 line 2976
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB2639 line 2977
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC2639 line 2978
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2639 line 2979
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2639 line 2981
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA2640 line 3170
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB2640 line 3171
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC2640 line 3172
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2640 line 3173
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2640 line 3175
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA2641 line 3364
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB2641 line 3365
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC2641 line 3366
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2641 line 3367
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2641 line 3369
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA2642 line 3558
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB2642 line 3559
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC2642 line 3560
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2642 line 3561
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2642 line 3563
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA2643 line 3752
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB2643 line 3753
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC2643 line 3754
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2643 line 3755
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2643 line 3757
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA2644 line 3946
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB2644 line 3947
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC2644 line 3948
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2644 line 3949
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2644 line 3951
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA2645 line 4140
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB2645 line 4141
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC2645 line 4142
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2645 line 4143
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2645 line 4145
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA2646 line 4334
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB2646 line 4335
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC2646 line 4336
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2646 line 4337
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2646 line 4339
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA2647 line 4528
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB2647 line 4529
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC2647 line 4530
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2647 line 4531
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2647 line 4533
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA2648 line 4722
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB2648 line 4723
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC2648 line 4724
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2648 line 4725
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2648 line 4727
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA2649 line 4916
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB2649 line 4917
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC2649 line 4918
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2649 line 4919
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2649 line 4921
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA2650 line 5110
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB2650 line 5111
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC2650 line 5112
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2650 line 5113
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2650 line 5115
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA2651 line 5304
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB2651 line 5305
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC2651 line 5306
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2651 line 5307
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2651 line 5309
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA2652 line 5498
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB2652 line 5499
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC2652 line 5500
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2652 line 5501
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2652 line 5503
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA2653 line 5692
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB2653 line 5693
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC2653 line 5694
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2653 line 5695
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2653 line 5697
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA2654 line 5886
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB2654 line 5887
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC2654 line 5888
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2654 line 5889
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2654 line 5891
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA2655 line 6080
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB2655 line 6081
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC2655 line 6082
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2655 line 6083
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2655 line 6085