OAI/Analysis/MutuallyUnbiased/MixedTargets/ReductionMergeData33.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1056 line 12
  2. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1056 line 14
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1056Check line 16
  4. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1057 line 18
  5. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1057 line 20
  6. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1057Check line 22
  7. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1058 line 24
  8. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1058 line 26
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1058Check line 28
  10. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1059 line 30
  11. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1059 line 32
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1059Check line 34
  13. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1060 line 36
  14. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1060 line 38
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1060Check line 40
  16. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1061 line 42
  17. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1061 line 44
  18. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1061Check line 46
  19. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1062 line 48
  20. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1062 line 50
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1062Check line 52
  22. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1063 line 54
  23. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1063 line 56
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1063Check line 58
  25. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1064 line 60
  26. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1064 line 62
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1064Check line 64
  28. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1065 line 66
  29. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1065 line 68
  30. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1065Check line 70
  31. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1066 line 72
  32. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1066 line 74
  33. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1066Check line 76
  34. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1067 line 78
  35. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1067 line 80
  36. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1067Check line 82
  37. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1068 line 84
  38. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1068 line 86
  39. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1068Check line 88
  40. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1069 line 90
  41. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1069 line 92
  42. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1069Check line 94
  43. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1070 line 96
  44. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1070 line 98
  45. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1070Check line 100
  46. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1071 line 102
  47. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1071 line 104
  48. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1071Check line 106
  49. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1072 line 108
  50. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1072 line 110
  51. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1072Check line 112
  52. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1073 line 114
  53. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1073 line 116
  54. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1073Check line 118
  55. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1074 line 120
  56. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1074 line 122
  57. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1074Check line 124
  58. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1075 line 126
  59. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1075 line 128
  60. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1075Check line 130
  61. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1076 line 132
  62. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1076 line 134
  63. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1076Check line 136
  64. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1077 line 138
  65. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1077 line 140
  66. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1077Check line 142
  67. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1078 line 144
  68. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1078 line 146
  69. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1078Check line 148
  70. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1079 line 150
  71. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1079 line 152
  72. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1079Check line 154
  73. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1080 line 156
  74. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1080 line 158
  75. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1080Check line 160
  76. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1081 line 162
  77. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1081 line 164
  78. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1081Check line 166
  79. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1082 line 168
  80. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1082 line 170
  81. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1082Check line 172
  82. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1083 line 174
  83. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1083 line 176
  84. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1083Check line 178
  85. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1084 line 180
  86. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1084 line 182
  87. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1084Check line 184
  88. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1085 line 186
  89. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1085 line 188
  90. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1085Check line 190
  91. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1086 line 192
  92. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1086 line 194
  93. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1086Check line 196
  94. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1087 line 198
  95. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1087 line 200
  96. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1087Check line 202