OAI/Computability/PerfectCompleteness/Decoding/CleanPhysicalDecoderLaw.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.F2 line 19
  2. def OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.inputOfArrays line 32
  3. theorem OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.inputOfArrays_heq line 41
  4. theorem OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.replayKnown_heq line 56
  5. def OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.uncastTape line 70
  6. def OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.inputFromTape line 79
  7. theorem OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.inputFromTape_eq_ownInput line 93
  8. def OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.adviceLaw line 110
  9. theorem OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.adviceLaw_heq line 125
  10. theorem OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.rightLaw_heq line 137
  11. abbrev OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.Answers line 151
  12. instance OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.answersFintype line 156
  13. def OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.answerEquiv line 164
  14. theorem OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.product_heq line 171
  15. theorem OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.pushforward_answerEquiv line 185
  16. theorem OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.meeting_answerEquiv line 196
  17. abbrev OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.lower line 218
  18. abbrev OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.leftArrays line 221
  19. abbrev OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.rightArrays line 225
  20. abbrev OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.rightWholeTape line 229
  21. def OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.rightInput line 233
  22. theorem OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.rightInput_eq_ownInput line 239
  23. def OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.useful line 252
  24. def OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.leftLaw line 261
  25. def OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.rightLaw line 264
  26. def OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.pairKernel line 268
  27. theorem OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.leftKernel_heq line 273
  28. theorem OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.rightKnownBuckets_heq line 281
  29. theorem OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.rightInput_heq line 306
  30. theorem OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.rightKernel_heq line 319
  31. theorem OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.pairKernel_heq line 326
  32. def OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.physicalAnswerEquiv line 335
  33. theorem OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.pairKernel_pushforward line 341
  34. theorem OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.probability_pairKernel line 349
  35. abbrev OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.physicalProjection line 358
  36. theorem OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.projection_heq line 362
  37. theorem OAI.PerfectCompleteness.CleanPhysicalDecoderLaw.meeting_probability_eq line 369