OAI/Computability/PerfectCompleteness/Sampling/CompletedSignedLaw.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.CompletedSignedLaw.SignedCompleted line 37
  2. abbrev OAI.PerfectCompleteness.CompletedSignedLaw.Completed line 45
  3. theorem OAI.PerfectCompleteness.CompletedSignedLaw.size_eq_active line 50
  4. def OAI.PerfectCompleteness.CompletedSignedLaw.completedEquiv line 56
  5. theorem OAI.PerfectCompleteness.CompletedSignedLaw.completedEquiv_apply line 69
  6. theorem OAI.PerfectCompleteness.CompletedSignedLaw.completedEquiv_source line 76
  7. theorem OAI.PerfectCompleteness.CompletedSignedLaw.completedEquiv_symm_source line 80
  8. theorem OAI.PerfectCompleteness.CompletedSignedLaw.descriptorTable_eq_map line 87
  9. def OAI.PerfectCompleteness.CompletedSignedLaw.law line 96
  10. theorem OAI.PerfectCompleteness.CompletedSignedLaw.completed_weight line 102
  11. theorem OAI.PerfectCompleteness.CompletedSignedLaw.actualcompletedLaw_transport line 120
  12. theorem OAI.PerfectCompleteness.CompletedSignedLaw.probability_reindex line 138
  13. theorem OAI.PerfectCompleteness.CompletedSignedLaw.probability_eq line 148
  14. theorem OAI.PerfectCompleteness.CompletedSignedLaw.probability_iterated line 158
  15. theorem OAI.PerfectCompleteness.CompletedSignedLaw.probability_schedule line 171