OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources15.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA480 line 25
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB480 line 26
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC480 line 27
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm480 line 28
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq480 line 30
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA481 line 81
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB481 line 82
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC481 line 83
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm481 line 84
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq481 line 86
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA482 line 137
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB482 line 138
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC482 line 139
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm482 line 140
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq482 line 142
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA483 line 331
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB483 line 332
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC483 line 333
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm483 line 334
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq483 line 336
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA484 line 525
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB484 line 526
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC484 line 527
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm484 line 528
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq484 line 530
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA485 line 719
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB485 line 720
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC485 line 721
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm485 line 722
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq485 line 724
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA486 line 775
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB486 line 776
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC486 line 777
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm486 line 778
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq486 line 780
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA487 line 831
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB487 line 832
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC487 line 833
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm487 line 834
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq487 line 836
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA488 line 887
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB488 line 888
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC488 line 889
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm488 line 890
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq488 line 892
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA489 line 943
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB489 line 944
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC489 line 945
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm489 line 946
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq489 line 948
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA490 line 999
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB490 line 1000
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC490 line 1001
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm490 line 1002
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq490 line 1004
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA491 line 1055
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB491 line 1056
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC491 line 1057
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm491 line 1058
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq491 line 1060
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA492 line 1249
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB492 line 1250
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC492 line 1251
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm492 line 1252
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq492 line 1254
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA493 line 1443
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB493 line 1444
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC493 line 1445
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm493 line 1446
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq493 line 1448
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA494 line 1637
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB494 line 1638
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC494 line 1639
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm494 line 1640
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq494 line 1642
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA495 line 1831
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB495 line 1832
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC495 line 1833
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm495 line 1834
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq495 line 1836
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA496 line 2025
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB496 line 2026
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC496 line 2027
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm496 line 2028
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq496 line 2030
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA497 line 2081
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB497 line 2082
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC497 line 2083
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm497 line 2084
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq497 line 2086
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA498 line 2137
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB498 line 2138
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC498 line 2139
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm498 line 2140
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq498 line 2142
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA499 line 2193
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB499 line 2194
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC499 line 2195
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm499 line 2196
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq499 line 2198
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA500 line 2387
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB500 line 2388
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC500 line 2389
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm500 line 2390
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq500 line 2392
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA501 line 2581
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB501 line 2582
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC501 line 2583
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm501 line 2584
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq501 line 2586
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA502 line 2775
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB502 line 2776
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC502 line 2777
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm502 line 2778
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq502 line 2780
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA503 line 2969
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB503 line 2970
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC503 line 2971
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm503 line 2972
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq503 line 2974
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA504 line 3163
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB504 line 3164
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC504 line 3165
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm504 line 3166
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq504 line 3168
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA505 line 3219
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB505 line 3220
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC505 line 3221
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm505 line 3222
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq505 line 3224
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA506 line 3275
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB506 line 3276
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC506 line 3277
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm506 line 3278
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq506 line 3280
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA507 line 3331
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB507 line 3332
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC507 line 3333
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm507 line 3334
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq507 line 3336
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA508 line 3387
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB508 line 3388
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC508 line 3389
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm508 line 3390
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq508 line 3392
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA509 line 3443
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB509 line 3444
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC509 line 3445
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm509 line 3446
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq509 line 3448
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA510 line 3499
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB510 line 3500
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC510 line 3501
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm510 line 3502
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq510 line 3504
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA511 line 3693
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB511 line 3694
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC511 line 3695
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm511 line 3696
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq511 line 3698