OAI/Analysis/MutuallyUnbiased/MixedData/Expression.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.denominator line 8
  2. theorem OAI.MUB6.Certificate.MixedData.denominator_pos line 10
  3. def OAI.MUB6.Certificate.MixedData.sourcePart0 line 12
  4. def OAI.MUB6.Certificate.MixedData.sourcePart1 line 14
  5. def OAI.MUB6.Certificate.MixedData.sourcePart2 line 16
  6. def OAI.MUB6.Certificate.MixedData.sourcePart3 line 18
  7. def OAI.MUB6.Certificate.MixedData.sourcePart4 line 20
  8. def OAI.MUB6.Certificate.MixedData.sourcePart5 line 22
  9. def OAI.MUB6.Certificate.MixedData.sourcePart6 line 24
  10. def OAI.MUB6.Certificate.MixedData.sourcePart7 line 26
  11. def OAI.MUB6.Certificate.MixedData.sourcePart8 line 28
  12. def OAI.MUB6.Certificate.MixedData.sourcePart9 line 30
  13. def OAI.MUB6.Certificate.MixedData.sourcePart10 line 32
  14. def OAI.MUB6.Certificate.MixedData.sourcePart11 line 34
  15. def OAI.MUB6.Certificate.MixedData.sourcePart12 line 36
  16. def OAI.MUB6.Certificate.MixedData.sourcePart13 line 38
  17. def OAI.MUB6.Certificate.MixedData.sourcePart14 line 40
  18. def OAI.MUB6.Certificate.MixedData.sourcePart15 line 42
  19. def OAI.MUB6.Certificate.MixedData.sourcePart16 line 44
  20. def OAI.MUB6.Certificate.MixedData.sourcePart17 line 46
  21. def OAI.MUB6.Certificate.MixedData.sourcePart18 line 48
  22. def OAI.MUB6.Certificate.MixedData.sourcePart19 line 50
  23. def OAI.MUB6.Certificate.MixedData.sourcePart20 line 52
  24. def OAI.MUB6.Certificate.MixedData.sourcePart21 line 54
  25. def OAI.MUB6.Certificate.MixedData.sourcePart22 line 56
  26. def OAI.MUB6.Certificate.MixedData.sourcePart23 line 58
  27. def OAI.MUB6.Certificate.MixedData.sourcePart24 line 60
  28. def OAI.MUB6.Certificate.MixedData.sourcePart25 line 62
  29. def OAI.MUB6.Certificate.MixedData.sourcePart26 line 64
  30. def OAI.MUB6.Certificate.MixedData.sourcePart27 line 66
  31. def OAI.MUB6.Certificate.MixedData.sourcePart28 line 68
  32. def OAI.MUB6.Certificate.MixedData.sourcePart29 line 70
  33. def OAI.MUB6.Certificate.MixedData.sourcePart30 line 72
  34. def OAI.MUB6.Certificate.MixedData.sourcePart31 line 74
  35. def OAI.MUB6.Certificate.MixedData.sourcePart32 line 76
  36. def OAI.MUB6.Certificate.MixedData.sourcePart33 line 78
  37. def OAI.MUB6.Certificate.MixedData.sourcePart34 line 80
  38. def OAI.MUB6.Certificate.MixedData.sourcePart35 line 82
  39. def OAI.MUB6.Certificate.MixedData.sourcePart36 line 84
  40. def OAI.MUB6.Certificate.MixedData.sourcePart37 line 86
  41. def OAI.MUB6.Certificate.MixedData.sourcePart38 line 88
  42. def OAI.MUB6.Certificate.MixedData.sourcePart39 line 90
  43. def OAI.MUB6.Certificate.MixedData.sourcePart40 line 92
  44. def OAI.MUB6.Certificate.MixedData.sourcePart41 line 94
  45. def OAI.MUB6.Certificate.MixedData.sourcePart42 line 96
  46. def OAI.MUB6.Certificate.MixedData.sourcePart43 line 98
  47. def OAI.MUB6.Certificate.MixedData.sourcePart44 line 100
  48. def OAI.MUB6.Certificate.MixedData.sourcePart45 line 102
  49. def OAI.MUB6.Certificate.MixedData.sourcePart46 line 104
  50. def OAI.MUB6.Certificate.MixedData.sourcePart47 line 106
  51. def OAI.MUB6.Certificate.MixedData.sourcePart48 line 108
  52. def OAI.MUB6.Certificate.MixedData.sourcePart49 line 110
  53. def OAI.MUB6.Certificate.MixedData.sourcePart50 line 112
  54. def OAI.MUB6.Certificate.MixedData.sourcePart51 line 114
  55. def OAI.MUB6.Certificate.MixedData.sourcePart52 line 116
  56. def OAI.MUB6.Certificate.MixedData.sourcePart53 line 118
  57. def OAI.MUB6.Certificate.MixedData.sourcePart54 line 120
  58. def OAI.MUB6.Certificate.MixedData.sourcePart55 line 122
  59. def OAI.MUB6.Certificate.MixedData.sourcePart56 line 124
  60. def OAI.MUB6.Certificate.MixedData.sourcePart57 line 126
  61. def OAI.MUB6.Certificate.MixedData.sourcePart58 line 128
  62. def OAI.MUB6.Certificate.MixedData.sourcePart59 line 130
  63. def OAI.MUB6.Certificate.MixedData.sourcePart60 line 132
  64. def OAI.MUB6.Certificate.MixedData.sourcePart61 line 134
  65. def OAI.MUB6.Certificate.MixedData.sourcePart62 line 136
  66. def OAI.MUB6.Certificate.MixedData.sourcePart63 line 138
  67. def OAI.MUB6.Certificate.MixedData.sourcePart64 line 140
  68. def OAI.MUB6.Certificate.MixedData.sourcePart65 line 142
  69. def OAI.MUB6.Certificate.MixedData.sourcePart66 line 144
  70. def OAI.MUB6.Certificate.MixedData.sourcePart67 line 146
  71. def OAI.MUB6.Certificate.MixedData.sourcePart68 line 148
  72. def OAI.MUB6.Certificate.MixedData.sourcePart69 line 150
  73. def OAI.MUB6.Certificate.MixedData.sourcePart70 line 152
  74. def OAI.MUB6.Certificate.MixedData.sourcePart71 line 154
  75. def OAI.MUB6.Certificate.MixedData.sourcePart72 line 156
  76. def OAI.MUB6.Certificate.MixedData.sourcePart73 line 158
  77. def OAI.MUB6.Certificate.MixedData.sourcePart74 line 160
  78. def OAI.MUB6.Certificate.MixedData.sourcePart75 line 162
  79. def OAI.MUB6.Certificate.MixedData.sourceCombination line 164
  80. def OAI.MUB6.Certificate.MixedData.rawCombination line 166
  81. def OAI.MUB6.Certificate.MixedData.residualCombination line 168
  82. def OAI.MUB6.Certificate.MixedData.targetCombination line 170