OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources29.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA928 line 21
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB928 line 22
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC928 line 23
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm928 line 24
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq928 line 26
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA929 line 77
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB929 line 78
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC929 line 79
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm929 line 80
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq929 line 82
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA930 line 133
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB930 line 134
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC930 line 135
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm930 line 136
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq930 line 138
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA931 line 189
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB931 line 190
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC931 line 191
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm931 line 192
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq931 line 194
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA932 line 245
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB932 line 246
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC932 line 247
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm932 line 248
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq932 line 250
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA933 line 439
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB933 line 440
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC933 line 441
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm933 line 442
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq933 line 444
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA934 line 633
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB934 line 634
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC934 line 635
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm934 line 636
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq934 line 638
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA935 line 827
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB935 line 828
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC935 line 829
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm935 line 830
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq935 line 832
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA936 line 1021
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB936 line 1022
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC936 line 1023
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm936 line 1024
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq936 line 1026
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA937 line 1215
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB937 line 1216
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC937 line 1217
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm937 line 1218
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq937 line 1220
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA938 line 1409
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB938 line 1410
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC938 line 1411
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm938 line 1412
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq938 line 1414
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA939 line 1465
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB939 line 1466
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC939 line 1467
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm939 line 1468
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq939 line 1470
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA940 line 1521
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB940 line 1522
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC940 line 1523
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm940 line 1524
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq940 line 1526
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA941 line 1577
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB941 line 1578
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC941 line 1579
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm941 line 1580
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq941 line 1582
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA942 line 1771
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB942 line 1772
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC942 line 1773
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm942 line 1774
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq942 line 1776
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA943 line 1965
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB943 line 1966
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC943 line 1967
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm943 line 1968
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq943 line 1970
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA944 line 2159
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB944 line 2160
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC944 line 2161
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm944 line 2162
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq944 line 2164
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA945 line 2215
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB945 line 2216
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC945 line 2217
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm945 line 2218
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq945 line 2220
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA946 line 2271
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB946 line 2272
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC946 line 2273
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm946 line 2274
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq946 line 2276
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA947 line 2327
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB947 line 2328
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC947 line 2329
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm947 line 2330
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq947 line 2332
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA948 line 2383
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB948 line 2384
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC948 line 2385
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm948 line 2386
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq948 line 2388
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA949 line 2439
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB949 line 2440
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC949 line 2441
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm949 line 2442
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq949 line 2444
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA950 line 2495
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB950 line 2496
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC950 line 2497
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm950 line 2498
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq950 line 2500
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA951 line 2551
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB951 line 2552
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC951 line 2553
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm951 line 2554
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq951 line 2556
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA952 line 2607
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB952 line 2608
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC952 line 2609
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm952 line 2610
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq952 line 2612
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA953 line 2663
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB953 line 2664
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC953 line 2665
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm953 line 2666
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq953 line 2668
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA954 line 2857
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB954 line 2858
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC954 line 2859
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm954 line 2860
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq954 line 2862
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA955 line 3051
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB955 line 3052
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC955 line 3053
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm955 line 3054
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq955 line 3056
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA956 line 3245
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB956 line 3246
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC956 line 3247
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm956 line 3248
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq956 line 3250
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA957 line 3301
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB957 line 3302
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC957 line 3303
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm957 line 3304
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq957 line 3306
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA958 line 3357
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB958 line 3358
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC958 line 3359
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm958 line 3360
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq958 line 3362
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA959 line 3413
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB959 line 3414
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC959 line 3415
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm959 line 3416
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq959 line 3418