OAI/Analysis/MutuallyUnbiased/MixedTargets/ReductionMergeData48.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1536 line 12
  2. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1536 line 14
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1536Check line 16
  4. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1537 line 18
  5. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1537 line 20
  6. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1537Check line 22
  7. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1538 line 24
  8. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1538 line 26
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1538Check line 28
  10. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1539 line 30
  11. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1539 line 32
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1539Check line 34
  13. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1540 line 36
  14. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1540 line 38
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1540Check line 40
  16. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1541 line 42
  17. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1541 line 44
  18. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1541Check line 46
  19. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1542 line 48
  20. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1542 line 50
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1542Check line 52
  22. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1543 line 54
  23. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1543 line 56
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1543Check line 58
  25. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1544 line 60
  26. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1544 line 62
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1544Check line 64
  28. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1545 line 66
  29. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1545 line 68
  30. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1545Check line 70
  31. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1546 line 72
  32. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1546 line 74
  33. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1546Check line 76
  34. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1547 line 78
  35. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1547 line 80
  36. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1547Check line 82
  37. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1548 line 84
  38. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1548 line 86
  39. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1548Check line 88
  40. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1549 line 90
  41. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1549 line 92
  42. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1549Check line 94
  43. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1550 line 96
  44. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1550 line 98
  45. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1550Check line 100
  46. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1551 line 102
  47. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1551 line 104
  48. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1551Check line 106
  49. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1552 line 108
  50. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1552 line 110
  51. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1552Check line 112
  52. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1553 line 114
  53. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1553 line 116
  54. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1553Check line 118
  55. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1554 line 120
  56. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1554 line 122
  57. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1554Check line 124
  58. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1555 line 126
  59. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1555 line 128
  60. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1555Check line 130
  61. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1556 line 132
  62. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1556 line 134
  63. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1556Check line 136
  64. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1557 line 138
  65. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1557 line 140
  66. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1557Check line 142
  67. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1558 line 144
  68. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1558 line 146
  69. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1558Check line 148
  70. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1559 line 150
  71. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1559 line 152
  72. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1559Check line 154
  73. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1560 line 156
  74. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1560 line 158
  75. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1560Check line 160
  76. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1561 line 162
  77. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1561 line 164
  78. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1561Check line 166
  79. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1562 line 168
  80. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1562 line 170
  81. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1562Check line 172
  82. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1563 line 174
  83. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1563 line 176
  84. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1563Check line 178
  85. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1564 line 180
  86. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1564 line 182
  87. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1564Check line 184
  88. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1565 line 186
  89. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1565 line 188
  90. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1565Check line 190
  91. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1566 line 192
  92. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1566 line 194
  93. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1566Check line 196
  94. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1567 line 198
  95. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1567 line 200
  96. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1567Check line 202