OAI/Analysis/MutuallyUnbiased/Bases/SmallMatrices.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Explicit mutually unbiased bases from two- and three-dimensional unitary matrices.

  1. abbrev OAI.MUB6.ThreeSmall.Sq line 12
  2. def OAI.MUB6.ThreeSmall.H2 line 14
  3. def OAI.MUB6.ThreeSmall.G2 line 15
  4. def OAI.MUB6.ThreeSmall.H3 line 16
  5. def OAI.MUB6.ThreeSmall.G3 line 17
  6. def OAI.MUB6.ThreeSmall.normalize line 19
  7. def OAI.MUB6.ThreeSmall.A line 22
  8. def OAI.MUB6.ThreeSmall.B line 23
  9. lemma OAI.MUB6.ThreeSmall.normalizer_normSq line 25
  10. lemma OAI.MUB6.ThreeSmall.normalized_cross_entry line 31
  11. lemma OAI.MUB6.ThreeSmall.normalized_gram line 42
  12. lemma OAI.MUB6.ThreeSmall.normalized_entry_normSq line 54
  13. lemma OAI.MUB6.ThreeSmall.normalized_cross_normSq line 58
  14. lemma OAI.MUB6.ThreeSmall.cross_normSq_swap line 65
  15. lemma OAI.MUB6.ThreeSmall.H2_gram line 74
  16. lemma OAI.MUB6.ThreeSmall.G2_gram line 80
  17. lemma OAI.MUB6.ThreeSmall.H3_gram line 86
  18. lemma OAI.MUB6.ThreeSmall.G3_gram line 94
  19. lemma OAI.MUB6.ThreeSmall.H2_unit line 112
  20. lemma OAI.MUB6.ThreeSmall.G2_unit line 114
  21. lemma OAI.MUB6.ThreeSmall.H3_unit line 116
  22. lemma OAI.MUB6.ThreeSmall.G3_unit line 118
  23. lemma OAI.MUB6.ThreeSmall.H2_G2_cross line 122
  24. lemma OAI.MUB6.ThreeSmall.omega_sq_reduce line 128
  25. lemma OAI.MUB6.ThreeSmall.omega_seven line 130
  26. lemma OAI.MUB6.ThreeSmall.omega_eight line 134
  27. lemma OAI.MUB6.ThreeSmall.omega_pow_mod3 line 139
  28. lemma OAI.MUB6.ThreeSmall.H3_G3_cross line 142
  29. theorem OAI.MUB6.ThreeSmall.A_gram line 155
  30. theorem OAI.MUB6.ThreeSmall.B_gram line 160
  31. lemma OAI.MUB6.ThreeSmall.A01 line 166
  32. lemma OAI.MUB6.ThreeSmall.A02 line 168
  33. lemma OAI.MUB6.ThreeSmall.A12 line 170
  34. lemma OAI.MUB6.ThreeSmall.B01 line 174
  35. lemma OAI.MUB6.ThreeSmall.B02 line 176
  36. lemma OAI.MUB6.ThreeSmall.B12 line 178
  37. theorem OAI.MUB6.ThreeSmall.A_cross_normSq line 183
  38. theorem OAI.MUB6.ThreeSmall.B_cross_normSq line 194