OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources76.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA2432 line 46
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB2432 line 47
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC2432 line 48
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2432 line 49
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2432 line 51
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA2433 line 240
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB2433 line 241
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC2433 line 242
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2433 line 243
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2433 line 245
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA2434 line 434
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB2434 line 435
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC2434 line 436
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2434 line 437
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2434 line 439
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA2435 line 490
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB2435 line 491
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC2435 line 492
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2435 line 493
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2435 line 495
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA2436 line 546
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB2436 line 547
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC2436 line 548
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2436 line 549
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2436 line 551
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA2437 line 602
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB2437 line 603
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC2437 line 604
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2437 line 605
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2437 line 607
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA2438 line 658
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB2438 line 659
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC2438 line 660
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2438 line 661
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2438 line 663
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA2439 line 852
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB2439 line 853
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC2439 line 854
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2439 line 855
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2439 line 857
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA2440 line 1046
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB2440 line 1047
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC2440 line 1048
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2440 line 1049
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2440 line 1051
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA2441 line 1240
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB2441 line 1241
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC2441 line 1242
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2441 line 1243
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2441 line 1245
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA2442 line 1296
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB2442 line 1297
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC2442 line 1298
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2442 line 1299
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2442 line 1301
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA2443 line 1490
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB2443 line 1491
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC2443 line 1492
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2443 line 1493
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2443 line 1495
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA2444 line 1684
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB2444 line 1685
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC2444 line 1686
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2444 line 1687
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2444 line 1689
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA2445 line 1878
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB2445 line 1879
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC2445 line 1880
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2445 line 1881
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2445 line 1883
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA2446 line 2072
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB2446 line 2073
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC2446 line 2074
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2446 line 2075
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2446 line 2077
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA2447 line 2266
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB2447 line 2267
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC2447 line 2268
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2447 line 2269
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2447 line 2271
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA2448 line 2322
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB2448 line 2323
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC2448 line 2324
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2448 line 2325
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2448 line 2327
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA2449 line 2516
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB2449 line 2517
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC2449 line 2518
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2449 line 2519
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2449 line 2521
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA2450 line 2710
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB2450 line 2711
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC2450 line 2712
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2450 line 2713
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2450 line 2715
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA2451 line 2904
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB2451 line 2905
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC2451 line 2906
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2451 line 2907
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2451 line 2909
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA2452 line 3098
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB2452 line 3099
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC2452 line 3100
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2452 line 3101
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2452 line 3103
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA2453 line 3292
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB2453 line 3293
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC2453 line 3294
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2453 line 3295
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2453 line 3297
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA2454 line 3486
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB2454 line 3487
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC2454 line 3488
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2454 line 3489
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2454 line 3491
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA2455 line 3542
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB2455 line 3543
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC2455 line 3544
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2455 line 3545
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2455 line 3547
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA2456 line 3598
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB2456 line 3599
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC2456 line 3600
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2456 line 3601
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2456 line 3603
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA2457 line 3792
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB2457 line 3793
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC2457 line 3794
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2457 line 3795
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2457 line 3797
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA2458 line 3986
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB2458 line 3987
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC2458 line 3988
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2458 line 3989
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2458 line 3991
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA2459 line 4180
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB2459 line 4181
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC2459 line 4182
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2459 line 4183
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2459 line 4185
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA2460 line 4236
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB2460 line 4237
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC2460 line 4238
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2460 line 4239
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2460 line 4241
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA2461 line 4292
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB2461 line 4293
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC2461 line 4294
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2461 line 4295
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2461 line 4297
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA2462 line 4486
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB2462 line 4487
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC2462 line 4488
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2462 line 4489
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2462 line 4491
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA2463 line 4680
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB2463 line 4681
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC2463 line 4682
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2463 line 4683
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2463 line 4685