OAI/Probability/SignedSweeps/MarkedSites.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SignedSweeps.MarkedAssignment line 10
  2. def OAI.SignedSweeps.moveMarks line 12
  3. lemma OAI.SignedSweeps.moveMarks_apply line 15
  4. lemma OAI.SignedSweeps.moveMarks_one line 18
  5. lemma OAI.SignedSweeps.moveMarks_mul line 21
  6. abbrev OAI.SignedSweeps.MarkedComplement line 25
  7. lemma OAI.SignedSweeps.markedComplement_card line 28
  8. def OAI.SignedSweeps.markedSites line 36
  9. def OAI.SignedSweeps.markedInjection line 40
  10. lemma OAI.SignedSweeps.markedInjection_apply line 43
  11. lemma OAI.SignedSweeps.markedInjection_avoids line 47
  12. def OAI.SignedSweeps.moveComplement line 51
  13. def OAI.SignedSweeps.markedSpinTransport line 63
  14. lemma OAI.SignedSweeps.markedSpinTransport_sites line 67
  15. lemma OAI.SignedSweeps.markedSpinTransport_one line 76
  16. lemma OAI.SignedSweeps.markedSpinTransport_mul line 83
  17. def OAI.SignedSweeps.moveMarksEquiv line 97
  18. lemma OAI.SignedSweeps.moveMarksEquiv_apply line 104
  19. def OAI.SignedSweeps.markedAllSites line 107
  20. lemma OAI.SignedSweeps.markedAllSites_left line 112
  21. lemma OAI.SignedSweeps.markedAllSites_right line 115
  22. lemma OAI.SignedSweeps.moveMarks_viaEmbedding line 118
  23. lemma OAI.SignedSweeps.markedSpinTransport_viaEmbedding line 126