OAI/Computability/PerfectCompleteness/Decoding/CleanDecoderSeedLawLemmas.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.CleanDecoderSeedLaw.F2 line 17
  2. abbrev OAI.PerfectCompleteness.CleanDecoderSeedLaw.LeftAnswer line 23
  3. abbrev OAI.PerfectCompleteness.CleanDecoderSeedLaw.RightAnswer line 26
  4. abbrev OAI.PerfectCompleteness.CleanDecoderSeedLaw.Seed line 42
  5. instance OAI.PerfectCompleteness.CleanDecoderSeedLaw.seedFintype line 44
  6. def OAI.PerfectCompleteness.CleanDecoderSeedLaw.leftKernel line 55
  7. def OAI.PerfectCompleteness.CleanDecoderSeedLaw.rightKernel line 58
  8. def OAI.PerfectCompleteness.CleanDecoderSeedLaw.leftSeedLaw line 63
  9. def OAI.PerfectCompleteness.CleanDecoderSeedLaw.rightSeedLaw line 66
  10. def OAI.PerfectCompleteness.CleanDecoderSeedLaw.seedLaw line 71
  11. theorem OAI.PerfectCompleteness.CleanDecoderSeedLaw.seedLaw_eq_dependent line 74
  12. theorem OAI.PerfectCompleteness.CleanDecoderSeedLaw.read_law line 79
  13. theorem OAI.PerfectCompleteness.CleanDecoderSeedLaw.probability_read line 87
  14. theorem OAI.PerfectCompleteness.CleanDecoderSeedLaw.supported_left line 101
  15. theorem OAI.PerfectCompleteness.CleanDecoderSeedLaw.supported_right line 110
  16. theorem OAI.PerfectCompleteness.CleanDecoderSeedLaw.supported_left_row line 119
  17. theorem OAI.PerfectCompleteness.CleanDecoderSeedLaw.supported_right_row line 126
  18. theorem OAI.PerfectCompleteness.CleanDecoderSeedLaw.supported_output_normalized line 135
  19. theorem OAI.PerfectCompleteness.CleanDecoderSeedLaw.supported_form_tested_rank line 144
  20. abbrev OAI.PerfectCompleteness.OriginalDecoderMark.SlotFamily line 172
  21. structure OAI.PerfectCompleteness.OriginalDecoderMark.Family line 175
  22. def OAI.PerfectCompleteness.OriginalDecoderMark.mark line 185
  23. theorem OAI.PerfectCompleteness.OriginalDecoderMark.mark_heq line 191
  24. theorem OAI.PerfectCompleteness.OriginalDecoderMark.mark_congr line 202
  25. theorem OAI.PerfectCompleteness.OriginalDecoderMark.table_eq_original line 218
  26. def OAI.PerfectCompleteness.OriginalDecoderMark.useful line 228
  27. theorem OAI.PerfectCompleteness.OriginalDecoderMark.useful_heq line 233
  28. theorem OAI.PerfectCompleteness.OriginalDecoderMark.useful_at_quotientMatrix line 242
  29. theorem OAI.PerfectCompleteness.OriginalDecoderMark.law_eq_adviceLaw line 252