OAI/Computability/PerfectCompleteness/Decoding/FixedStoppedDecoderLaw.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.FixedStoppedDecoderLaw.familySampleFintype line 20
  2. abbrev OAI.PerfectCompleteness.FixedStoppedDecoderLaw.Context line 33
  3. def OAI.PerfectCompleteness.FixedStoppedDecoderLaw.labeling line 35
  4. def OAI.PerfectCompleteness.FixedStoppedDecoderLaw.flag line 43
  5. def OAI.PerfectCompleteness.FixedStoppedDecoderLaw.markFamily line 49
  6. abbrev OAI.PerfectCompleteness.FixedStoppedDecoderLaw.setups line 58
  7. def OAI.PerfectCompleteness.FixedStoppedDecoderLaw.useful line 62
  8. def OAI.PerfectCompleteness.FixedStoppedDecoderLaw.threshold line 76
  9. abbrev OAI.PerfectCompleteness.FixedStoppedDecoderLaw.Sample line 80
  10. def OAI.PerfectCompleteness.FixedStoppedDecoderLaw.law line 85
  11. abbrev OAI.PerfectCompleteness.FixedStoppedDecoderLaw.meeting line 94
  12. abbrev OAI.PerfectCompleteness.FixedStoppedDecoderLaw.lowAgreement line 97
  13. abbrev OAI.PerfectCompleteness.FixedStoppedDecoderLaw.highAgreement line 102
  14. theorem OAI.PerfectCompleteness.FixedStoppedDecoderLaw.probability_split line 107
  15. theorem OAI.PerfectCompleteness.FixedStoppedDecoderLaw.low_probability_lt_accuracy line 122