OAI/Computability/PerfectCompleteness/Repetition/CleanPhysicalProjectedMeeting.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.CleanPhysicalProjectedMeeting.F2 line 17
  2. theorem OAI.PerfectCompleteness.CleanPhysicalProjectedMeeting.evaluate_uncastTape line 25
  3. abbrev OAI.PerfectCompleteness.CleanPhysicalProjectedMeeting.lower line 43
  4. def OAI.PerfectCompleteness.CleanPhysicalProjectedMeeting.rawSample line 45
  5. abbrev OAI.PerfectCompleteness.CleanPhysicalProjectedMeeting.visible line 52
  6. theorem OAI.PerfectCompleteness.CleanPhysicalProjectedMeeting.raw_arrays line 55
  7. theorem OAI.PerfectCompleteness.CleanPhysicalProjectedMeeting.projected_raw_arrays line 65
  8. theorem OAI.PerfectCompleteness.CleanPhysicalProjectedMeeting.rightInput_eq_readInput line 75
  9. theorem OAI.PerfectCompleteness.CleanPhysicalProjectedMeeting.leftLaw_eq_visible line 90
  10. def OAI.PerfectCompleteness.CleanPhysicalProjectedMeeting.visiblePairKernel line 115
  11. theorem OAI.PerfectCompleteness.CleanPhysicalProjectedMeeting.pairKernel_eq_visible line 135
  12. theorem OAI.PerfectCompleteness.CleanPhysicalProjectedMeeting.meeting_probability_eq line 143