OAI/Analysis/MutuallyUnbiased/MixedMoments/MixedShifts.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.sampledMatrix line 12
  2. theorem OAI.MUB6.sampledMatrix_isHadamard line 15
  3. theorem OAI.MUB6.sampledMatrix_cross line 21
  4. def OAI.MUB6.tripleCharges line 30
  5. def OAI.MUB6.doubleCharges line 33
  6. theorem OAI.MUB6.mixedIntegrand_three line 35
  7. theorem OAI.MUB6.mixedIntegrand_two line 43
  8. theorem OAI.MUB6.mixedMoment_same line 49
  9. theorem OAI.MUB6.mixedMoment_same_reversed line 63
  10. theorem OAI.MUB6.average_finset_sum line 79
  11. theorem OAI.MUB6.average_offDiagSum line 86
  12. theorem OAI.MUB6.mixedMoment_different line 90