OAI/Analysis/MutuallyUnbiased/Moments/GramNormalization.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Row permutation and symmetry normalization of auxiliary Gram terms. The normalizer is executable, but its interpretation theorem is an ordinary proof valid for arbitrary complex mutually unbiased bases.

  1. structure OAI.MUB6.GramNormalization.Key line 15
  2. def OAI.MUB6.GramNormalization.rowOrder line 21
  3. def OAI.MUB6.GramNormalization.orderedKey line 24
  4. def OAI.MUB6.GramNormalization.normalize line 27
  5. def OAI.MUB6.GramNormalization.Key.leftCharge line 32
  6. def OAI.MUB6.GramNormalization.Key.rightCharge line 33
  7. def OAI.MUB6.GramNormalization.eval line 35
  8. theorem OAI.MUB6.GramNormalization.rowOrder_length line 38
  9. theorem OAI.MUB6.GramNormalization.rowOrder_nodup line 41
  10. def OAI.MUB6.GramNormalization.rowAt line 44
  11. theorem OAI.MUB6.GramNormalization.rowAt_injective line 47
  12. def OAI.MUB6.GramNormalization.rowPermutation line 52
  13. theorem OAI.MUB6.GramNormalization.orderedKey_leftCharge line 56
  14. theorem OAI.MUB6.GramNormalization.orderedKey_rightCharge line 63
  15. theorem OAI.MUB6.GramNormalization.auxiliaryMixedEntry_row_permutation line 70
  16. theorem OAI.MUB6.GramNormalization.auxiliaryMixedEntry_symm line 76
  17. theorem OAI.MUB6.GramNormalization.eval_orderedKey line 81
  18. theorem OAI.MUB6.GramNormalization.eval_normalize line 87