OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources19.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA608 line 29
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB608 line 30
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC608 line 31
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm608 line 32
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq608 line 34
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA609 line 85
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB609 line 86
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC609 line 87
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm609 line 88
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq609 line 90
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA610 line 279
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB610 line 280
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC610 line 281
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm610 line 282
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq610 line 284
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA611 line 473
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB611 line 474
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC611 line 475
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm611 line 476
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq611 line 478
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA612 line 667
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB612 line 668
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC612 line 669
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm612 line 670
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq612 line 672
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA613 line 861
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB613 line 862
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC613 line 863
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm613 line 864
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq613 line 866
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA614 line 1055
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB614 line 1056
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC614 line 1057
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm614 line 1058
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq614 line 1060
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA615 line 1249
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB615 line 1250
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC615 line 1251
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm615 line 1252
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq615 line 1254
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA616 line 1443
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB616 line 1444
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC616 line 1445
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm616 line 1446
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq616 line 1448
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA617 line 1637
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB617 line 1638
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC617 line 1639
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm617 line 1640
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq617 line 1642
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA618 line 1831
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB618 line 1832
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC618 line 1833
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm618 line 1834
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq618 line 1836
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA619 line 1887
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB619 line 1888
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC619 line 1889
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm619 line 1890
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq619 line 1892
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA620 line 1943
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB620 line 1944
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC620 line 1945
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm620 line 1946
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq620 line 1948
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA621 line 1999
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB621 line 2000
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC621 line 2001
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm621 line 2002
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq621 line 2004
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA622 line 2055
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB622 line 2056
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC622 line 2057
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm622 line 2058
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq622 line 2060
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA623 line 2249
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB623 line 2250
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC623 line 2251
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm623 line 2252
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq623 line 2254
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA624 line 2443
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB624 line 2444
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC624 line 2445
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm624 line 2446
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq624 line 2448
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA625 line 2637
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB625 line 2638
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC625 line 2639
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm625 line 2640
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq625 line 2642
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA626 line 2831
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB626 line 2832
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC626 line 2833
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm626 line 2834
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq626 line 2836
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA627 line 2887
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB627 line 2888
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC627 line 2889
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm627 line 2890
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq627 line 2892
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA628 line 3081
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB628 line 3082
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC628 line 3083
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm628 line 3084
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq628 line 3086
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA629 line 3275
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB629 line 3276
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC629 line 3277
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm629 line 3278
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq629 line 3280
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA630 line 3469
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB630 line 3470
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC630 line 3471
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm630 line 3472
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq630 line 3474
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA631 line 3663
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB631 line 3664
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC631 line 3665
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm631 line 3666
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq631 line 3668
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA632 line 3857
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB632 line 3858
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC632 line 3859
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm632 line 3860
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq632 line 3862
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA633 line 4051
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB633 line 4052
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC633 line 4053
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm633 line 4054
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq633 line 4056
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA634 line 4245
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB634 line 4246
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC634 line 4247
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm634 line 4248
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq634 line 4250
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA635 line 4439
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB635 line 4440
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC635 line 4441
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm635 line 4442
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq635 line 4444
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA636 line 4495
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB636 line 4496
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC636 line 4497
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm636 line 4498
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq636 line 4500
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA637 line 4689
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB637 line 4690
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC637 line 4691
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm637 line 4692
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq637 line 4694
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA638 line 4883
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB638 line 4884
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC638 line 4885
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm638 line 4886
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq638 line 4888
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA639 line 5077
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB639 line 5078
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC639 line 5079
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm639 line 5080
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq639 line 5082