OAI/Analysis/MutuallyUnbiased/Certificate/Interpretation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Reindexing and averaging preserve the interpretation of sparse forms. These algebraic facts connect finite checked coefficients to actual moments.

  1. def OAI.MUB6.Certificate.Sparse.reindex line 14
  2. theorem OAI.MUB6.Certificate.Sparse.eval_reindex line 17
  3. theorem OAI.MUB6.Certificate.Sparse.eval_average line 26
  4. def OAI.MUB6.Certificate.Integer.Sparse.reindex line 40
  5. theorem OAI.MUB6.Certificate.Integer.Sparse.eval_reindex line 43
  6. def OAI.MUB6.Certificate.Integer.Sparse.toRational line 52
  7. theorem OAI.MUB6.Certificate.Integer.Sparse.eval_toRational line 55
  8. theorem OAI.MUB6.Certificate.Integer.Sparse.eval_average line 65