OAI/Analysis/MutuallyUnbiased/Certificate/CompareMerge.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Sparse collection needs only a computable comparison, not order axioms. The comparison changes the representation but never its real evaluation.

  1. def OAI.MUB6.Certificate.Integer.Sparse.mergeByFuel line 11
  2. theorem OAI.MUB6.Certificate.Integer.Sparse.eval_mergeByFuel line 22
  3. def OAI.MUB6.Certificate.Integer.Sparse.mergeBy line 50
  4. theorem OAI.MUB6.Certificate.Integer.Sparse.eval_mergeBy line 53
  5. def OAI.MUB6.Certificate.Integer.Sparse.collect line 56
  6. theorem OAI.MUB6.Certificate.Integer.Sparse.eval_collect line 59
  7. theorem OAI.MUB6.Certificate.Integer.Sparse.eval_flatten line 69
  8. def OAI.MUB6.Certificate.Integer.Sparse.mergePairs line 75
  9. theorem OAI.MUB6.Certificate.Integer.Sparse.eval_mergePairs line 80
  10. def OAI.MUB6.Certificate.Integer.Sparse.collectLevels line 88
  11. theorem OAI.MUB6.Certificate.Integer.Sparse.eval_collectLevels line 94
  12. def OAI.MUB6.Certificate.Integer.Sparse.collectBalanced line 108
  13. theorem OAI.MUB6.Certificate.Integer.Sparse.eval_collectBalanced line 111