OAI/Analysis/MutuallyUnbiased/PairMoments/PairTermSums.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms0_at0 line 9
  2. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms0_at1 line 10
  3. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms0_at2 line 11
  4. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms0_at3 line 12
  5. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms0_at4 line 13
  6. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms0_at5 line 14
  7. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms0_at6 line 15
  8. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms0_at7 line 16
  9. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms0_at8 line 17
  10. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms0_at9 line 18
  11. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms0_at10 line 19
  12. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms0_at11 line 20
  13. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms0_at12 line 21
  14. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms0_at13 line 22
  15. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms0_at14 line 23
  16. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms0_at15 line 24
  17. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms0_at16 line 25
  18. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms0_at17 line 26
  19. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms0_at18 line 27
  20. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms0_at19 line 28
  21. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms0_at20 line 29
  22. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms0_at21 line 30
  23. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms0_at22 line 31
  24. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms0_at23 line 32
  25. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms0_at24 line 33
  26. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms0_at25 line 34
  27. theorem OAI.MUB6.Certificate.PairTargetSemantics.sum_terms0_expand line 35
  28. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms1_at0 line 41
  29. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms1_at1 line 42
  30. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms1_at2 line 43
  31. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms1_at3 line 44
  32. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms1_at4 line 45
  33. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms1_at5 line 46
  34. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms1_at6 line 47
  35. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms1_at7 line 48
  36. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms1_at8 line 49
  37. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms1_at9 line 50
  38. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms1_at10 line 51
  39. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms1_at11 line 52
  40. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms1_at12 line 53
  41. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms1_at13 line 54
  42. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms1_at14 line 55
  43. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms1_at15 line 56
  44. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms1_at16 line 57
  45. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms1_at17 line 58
  46. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms1_at18 line 59
  47. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms1_at19 line 60
  48. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms1_at20 line 61
  49. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms1_at21 line 62
  50. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms1_at22 line 63
  51. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms1_at23 line 64
  52. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms1_at24 line 65
  53. theorem OAI.MUB6.Certificate.PairTargetSemantics.sumterms1_at25 line 66
  54. theorem OAI.MUB6.Certificate.PairTargetSemantics.sum_terms1_expand line 67