OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources13.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA416 line 31
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB416 line 32
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC416 line 33
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm416 line 34
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq416 line 36
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA417 line 225
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB417 line 226
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC417 line 227
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm417 line 228
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq417 line 230
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA418 line 419
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB418 line 420
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC418 line 421
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm418 line 422
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq418 line 424
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA419 line 475
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB419 line 476
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC419 line 477
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm419 line 478
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq419 line 480
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA420 line 531
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB420 line 532
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC420 line 533
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm420 line 534
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq420 line 536
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA421 line 587
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB421 line 588
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC421 line 589
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm421 line 590
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq421 line 592
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA422 line 781
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB422 line 782
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC422 line 783
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm422 line 784
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq422 line 786
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA423 line 975
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB423 line 976
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC423 line 977
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm423 line 978
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq423 line 980
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA424 line 1169
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB424 line 1170
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC424 line 1171
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm424 line 1172
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq424 line 1174
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA425 line 1363
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB425 line 1364
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC425 line 1365
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm425 line 1366
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq425 line 1368
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA426 line 1557
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB426 line 1558
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC426 line 1559
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm426 line 1560
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq426 line 1562
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA427 line 1751
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB427 line 1752
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC427 line 1753
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm427 line 1754
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq427 line 1756
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA428 line 1945
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB428 line 1946
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC428 line 1947
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm428 line 1948
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq428 line 1950
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA429 line 2001
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB429 line 2002
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC429 line 2003
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm429 line 2004
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq429 line 2006
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA430 line 2057
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB430 line 2058
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC430 line 2059
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm430 line 2060
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq430 line 2062
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA431 line 2113
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB431 line 2114
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC431 line 2115
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm431 line 2116
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq431 line 2118
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA432 line 2169
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB432 line 2170
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC432 line 2171
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm432 line 2172
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq432 line 2174
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA433 line 2225
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB433 line 2226
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC433 line 2227
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm433 line 2228
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq433 line 2230
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA434 line 2419
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB434 line 2420
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC434 line 2421
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm434 line 2422
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq434 line 2424
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA435 line 2613
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB435 line 2614
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC435 line 2615
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm435 line 2616
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq435 line 2618
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA436 line 2807
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB436 line 2808
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC436 line 2809
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm436 line 2810
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq436 line 2812
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA437 line 3001
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB437 line 3002
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC437 line 3003
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm437 line 3004
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq437 line 3006
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA438 line 3195
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB438 line 3196
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC438 line 3197
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm438 line 3198
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq438 line 3200
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA439 line 3389
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB439 line 3390
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC439 line 3391
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm439 line 3392
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq439 line 3394
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA440 line 3583
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB440 line 3584
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC440 line 3585
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm440 line 3586
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq440 line 3588
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA441 line 3777
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB441 line 3778
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC441 line 3779
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm441 line 3780
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq441 line 3782
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA442 line 3971
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB442 line 3972
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC442 line 3973
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm442 line 3974
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq442 line 3976
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA443 line 4027
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB443 line 4028
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC443 line 4029
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm443 line 4030
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq443 line 4032
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA444 line 4083
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB444 line 4084
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC444 line 4085
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm444 line 4086
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq444 line 4088
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA445 line 4139
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB445 line 4140
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC445 line 4141
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm445 line 4142
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq445 line 4144
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA446 line 4195
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB446 line 4196
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC446 line 4197
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm446 line 4198
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq446 line 4200
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA447 line 4251
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB447 line 4252
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC447 line 4253
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm447 line 4254
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq447 line 4256