OAI/Computability/PerfectCompleteness/Sampling/FilledUniformSampler.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.FilledUniformSampler.Exterior line 22
  2. theorem OAI.PerfectCompleteness.FilledUniformSampler.cutSlots_fill line 25
  3. def OAI.PerfectCompleteness.FilledUniformSampler.exteriorEquiv line 30
  4. def OAI.PerfectCompleteness.FilledUniformSampler.childrenEquiv line 37
  5. theorem OAI.PerfectCompleteness.FilledUniformSampler.childrenEquiv_apply line 45
  6. theorem OAI.PerfectCompleteness.FilledUniformSampler.childrenEquiv_heq line 54
  7. def OAI.PerfectCompleteness.FilledUniformSampler.filledSplitEquiv line 61
  8. theorem OAI.PerfectCompleteness.FilledUniformSampler.filledSplitEquiv_apply line 69
  9. theorem OAI.PerfectCompleteness.FilledUniformSampler.filledSplitEquiv_tapeLaw line 78
  10. def OAI.PerfectCompleteness.FilledUniformSampler.evaluate line 95
  11. theorem OAI.PerfectCompleteness.FilledUniformSampler.evaluate_law line 102