OAI/Analysis/MutuallyUnbiased/PairTargets/Data.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MUB6.Certificate.PairTargetSemantics.Term line 9
  2. def OAI.MUB6.Certificate.PairTargetSemantics.weightedAverage line 15
  3. def OAI.MUB6.Certificate.PairTargetSemantics.term0 line 18
  4. def OAI.MUB6.Certificate.PairTargetSemantics.term1 line 20
  5. def OAI.MUB6.Certificate.PairTargetSemantics.term2 line 22
  6. def OAI.MUB6.Certificate.PairTargetSemantics.term3 line 24
  7. def OAI.MUB6.Certificate.PairTargetSemantics.term4 line 26
  8. def OAI.MUB6.Certificate.PairTargetSemantics.term5 line 28
  9. def OAI.MUB6.Certificate.PairTargetSemantics.term6 line 30
  10. def OAI.MUB6.Certificate.PairTargetSemantics.term7 line 32
  11. def OAI.MUB6.Certificate.PairTargetSemantics.term8 line 34
  12. def OAI.MUB6.Certificate.PairTargetSemantics.term9 line 36
  13. def OAI.MUB6.Certificate.PairTargetSemantics.term10 line 38
  14. def OAI.MUB6.Certificate.PairTargetSemantics.term11 line 40
  15. def OAI.MUB6.Certificate.PairTargetSemantics.term12 line 42
  16. def OAI.MUB6.Certificate.PairTargetSemantics.term13 line 44
  17. def OAI.MUB6.Certificate.PairTargetSemantics.term14 line 46
  18. def OAI.MUB6.Certificate.PairTargetSemantics.term15 line 48
  19. def OAI.MUB6.Certificate.PairTargetSemantics.term16 line 50
  20. def OAI.MUB6.Certificate.PairTargetSemantics.term17 line 52
  21. def OAI.MUB6.Certificate.PairTargetSemantics.term18 line 54
  22. def OAI.MUB6.Certificate.PairTargetSemantics.term19 line 56
  23. def OAI.MUB6.Certificate.PairTargetSemantics.term20 line 58
  24. def OAI.MUB6.Certificate.PairTargetSemantics.term21 line 60
  25. def OAI.MUB6.Certificate.PairTargetSemantics.term22 line 62
  26. def OAI.MUB6.Certificate.PairTargetSemantics.term23 line 64
  27. def OAI.MUB6.Certificate.PairTargetSemantics.term24 line 66
  28. def OAI.MUB6.Certificate.PairTargetSemantics.term25 line 68
  29. def OAI.MUB6.Certificate.PairTargetSemantics.term26 line 70
  30. def OAI.MUB6.Certificate.PairTargetSemantics.terms0 line 72
  31. def OAI.MUB6.Certificate.PairTargetSemantics.expanded0 line 75
  32. def OAI.MUB6.Certificate.PairTargetSemantics.terms1 line 77
  33. def OAI.MUB6.Certificate.PairTargetSemantics.expanded1 line 80