OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources0.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA0 line 19
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB0 line 20
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC0 line 21
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm0 line 22
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq0 line 24
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA1 line 213
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB1 line 214
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC1 line 215
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1 line 216
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1 line 218
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA2 line 407
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB2 line 408
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC2 line 409
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2 line 410
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2 line 412
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA3 line 601
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB3 line 602
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC3 line 603
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm3 line 604
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq3 line 606
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA4 line 795
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB4 line 796
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC4 line 797
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm4 line 798
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq4 line 800
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA5 line 989
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB5 line 990
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC5 line 991
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm5 line 992
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq5 line 994
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA6 line 1183
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB6 line 1184
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC6 line 1185
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm6 line 1186
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq6 line 1188
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA7 line 1239
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB7 line 1240
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC7 line 1241
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm7 line 1242
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq7 line 1244
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA8 line 1433
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB8 line 1434
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC8 line 1435
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm8 line 1436
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq8 line 1438
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA9 line 1489
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB9 line 1490
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC9 line 1491
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm9 line 1492
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq9 line 1494
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA10 line 1683
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB10 line 1684
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC10 line 1685
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm10 line 1686
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq10 line 1688
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA11 line 1877
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB11 line 1878
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC11 line 1879
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm11 line 1880
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq11 line 1882
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA12 line 2071
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB12 line 2072
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC12 line 2073
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm12 line 2074
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq12 line 2076
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA13 line 2265
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB13 line 2266
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC13 line 2267
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm13 line 2268
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq13 line 2270
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA14 line 2459
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB14 line 2460
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC14 line 2461
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm14 line 2462
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq14 line 2464
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA15 line 2653
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB15 line 2654
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC15 line 2655
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm15 line 2656
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq15 line 2658
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA16 line 2847
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB16 line 2848
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC16 line 2849
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm16 line 2850
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq16 line 2852
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA17 line 3041
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB17 line 3042
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC17 line 3043
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm17 line 3044
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq17 line 3046
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA18 line 3235
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB18 line 3236
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC18 line 3237
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm18 line 3238
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq18 line 3240
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA19 line 3429
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB19 line 3430
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC19 line 3431
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm19 line 3432
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq19 line 3434
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA20 line 3623
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB20 line 3624
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC20 line 3625
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm20 line 3626
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq20 line 3628
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA21 line 3817
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB21 line 3818
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC21 line 3819
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm21 line 3820
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq21 line 3822
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA22 line 4011
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB22 line 4012
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC22 line 4013
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm22 line 4014
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq22 line 4016
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA23 line 4205
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB23 line 4206
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC23 line 4207
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm23 line 4208
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq23 line 4210
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA24 line 4399
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB24 line 4400
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC24 line 4401
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm24 line 4402
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq24 line 4404
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA25 line 4593
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB25 line 4594
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC25 line 4595
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm25 line 4596
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq25 line 4598
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA26 line 4787
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB26 line 4788
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC26 line 4789
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm26 line 4790
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq26 line 4792
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA27 line 4981
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB27 line 4982
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC27 line 4983
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm27 line 4984
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq27 line 4986
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA28 line 5175
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB28 line 5176
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC28 line 5177
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm28 line 5178
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq28 line 5180
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA29 line 5369
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB29 line 5370
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC29 line 5371
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm29 line 5372
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq29 line 5374
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA30 line 5563
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB30 line 5564
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC30 line 5565
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm30 line 5566
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq30 line 5568
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA31 line 5757
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB31 line 5758
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC31 line 5759
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm31 line 5760
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq31 line 5762