OAI/Computability/PerfectCompleteness/Foundations/StoppedProjectedUsefulEvent.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.StoppedProjectedUsefulEvent.observe_assemble line 21
  2. theorem OAI.PerfectCompleteness.StoppedProjectedUsefulEvent.upper_observe_assemble line 41
  3. abbrev OAI.PerfectCompleteness.StoppedProjectedUsefulEvent.Outer line 84
  4. abbrev OAI.PerfectCompleteness.StoppedProjectedUsefulEvent.Inner line 86
  5. def OAI.PerfectCompleteness.StoppedProjectedUsefulEvent.upperLevel line 89
  6. abbrev OAI.PerfectCompleteness.StoppedProjectedUsefulEvent.chosen line 91
  7. abbrev OAI.PerfectCompleteness.StoppedProjectedUsefulEvent.continuation line 94
  8. theorem OAI.PerfectCompleteness.StoppedProjectedUsefulEvent.stepPath_eq line 97
  9. def OAI.PerfectCompleteness.StoppedProjectedUsefulEvent.stepTape line 105
  10. def OAI.PerfectCompleteness.StoppedProjectedUsefulEvent.readout line 113
  11. def OAI.PerfectCompleteness.StoppedProjectedUsefulEvent.background line 122
  12. def OAI.PerfectCompleteness.StoppedProjectedUsefulEvent.buckets line 131
  13. def OAI.PerfectCompleteness.StoppedProjectedUsefulEvent.upperDirection line 137
  14. theorem OAI.PerfectCompleteness.StoppedProjectedUsefulEvent.upperDirection_eq line 143
  15. abbrev OAI.PerfectCompleteness.StoppedProjectedUsefulEvent.experiment line 152
  16. def OAI.PerfectCompleteness.StoppedProjectedUsefulEvent.upperEvent line 155
  17. theorem OAI.PerfectCompleteness.StoppedProjectedUsefulEvent.arrays_readout line 167
  18. theorem OAI.PerfectCompleteness.StoppedProjectedUsefulEvent.usefulEvent_eq line 197