OAI/Computability/PerfectCompleteness/Decoding/DecoderFamilyLawLemmas.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.DecoderFamilyLaw.Fiber line 22
  2. abbrev OAI.PerfectCompleteness.DecoderFamilyLaw.Sample line 25
  3. def OAI.PerfectCompleteness.DecoderFamilyLaw.meeting line 27
  4. def OAI.PerfectCompleteness.DecoderFamilyLaw.lowAgreement line 32
  5. def OAI.PerfectCompleteness.DecoderFamilyLaw.highAgreement line 35
  6. def OAI.PerfectCompleteness.DecoderFamilyLaw.fiberLaw line 49
  7. def OAI.PerfectCompleteness.DecoderFamilyLaw.law line 54
  8. theorem OAI.PerfectCompleteness.DecoderFamilyLaw.probability_eq_expectation line 59
  9. theorem OAI.PerfectCompleteness.DecoderFamilyLaw.probability_split line 69
  10. theorem OAI.PerfectCompleteness.DecoderFamilyLaw.meeting_probability_ge line 84
  11. abbrev OAI.PerfectCompleteness.DecoderPairHighOutput.F2 line 110
  12. abbrev OAI.PerfectCompleteness.DecoderPairHighOutput.exposed line 116
  13. abbrev OAI.PerfectCompleteness.DecoderPairHighOutput.slots line 119
  14. abbrev OAI.PerfectCompleteness.DecoderPairHighOutput.background line 122
  15. abbrev OAI.PerfectCompleteness.DecoderPairHighOutput.advice line 125
  16. abbrev OAI.PerfectCompleteness.DecoderPairHighOutput.Answer line 129
  17. instance OAI.PerfectCompleteness.DecoderPairHighOutput.answerFintype line 132
  18. theorem OAI.PerfectCompleteness.DecoderPairHighOutput.actualInput_eq line 135
  19. abbrev OAI.PerfectCompleteness.DecoderPairHighOutput.output line 143
  20. abbrev OAI.PerfectCompleteness.DecoderPairHighOutput.decode line 148
  21. theorem OAI.PerfectCompleteness.DecoderPairHighOutput.nativeRank_eq_fullRank line 152
  22. theorem OAI.PerfectCompleteness.DecoderPairHighOutput.decode_of_highAgrees line 158
  23. theorem OAI.PerfectCompleteness.DecoderPairHighOutput.highAgrees_eq_highMeeting line 167
  24. theorem OAI.PerfectCompleteness.DecoderPairHighOutput.supported_left line 191
  25. theorem OAI.PerfectCompleteness.DecoderPairHighOutput.valid_of_support line 206
  26. theorem OAI.PerfectCompleteness.DecoderPairHighOutput.valid_output_of_highAgrees line 221
  27. theorem OAI.PerfectCompleteness.DecoderPairHighOutput.responseLaw_eq_pushforward line 232
  28. theorem OAI.PerfectCompleteness.DecoderPairHighOutput.pair_decode_law line 240
  29. theorem OAI.PerfectCompleteness.FixedDecoderFamilyRate.expectation_lt_const line 273
  30. def OAI.PerfectCompleteness.FixedDecoderFamilyRate.setups line 298
  31. theorem OAI.PerfectCompleteness.FixedDecoderFamilyRate.probability_lt_accuracy line 314
  32. theorem OAI.PerfectCompleteness.FixedDecoderFamilyContradiction.impossible line 360