OAI/Computability/PerfectCompleteness/Decoding/CleanDecoderRateLemmas.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.CleanDecoderRate.F2 line 19
  2. structure OAI.PerfectCompleteness.CleanDecoderRate.Setup line 21
  3. abbrev OAI.PerfectCompleteness.CleanDecoderRate.path line 35
  4. abbrev OAI.PerfectCompleteness.CleanDecoderRate.Calls line 36
  5. abbrev OAI.PerfectCompleteness.CleanDecoderRate.Record line 37
  6. abbrev OAI.PerfectCompleteness.CleanDecoderRate.Sample line 39
  7. def OAI.PerfectCompleteness.CleanDecoderRate.context line 42
  8. abbrev OAI.PerfectCompleteness.CleanDecoderRate.Seed line 46
  9. instance OAI.PerfectCompleteness.CleanDecoderRate.seedFintype line 48
  10. abbrev OAI.PerfectCompleteness.CleanDecoderRate.observations line 51
  11. abbrev OAI.PerfectCompleteness.CleanDecoderRate.sources line 54
  12. def OAI.PerfectCompleteness.CleanDecoderRate.rawLaw line 57
  13. def OAI.PerfectCompleteness.CleanDecoderRate.kernel line 69
  14. def OAI.PerfectCompleteness.CleanDecoderRate.law line 72
  15. def OAI.PerfectCompleteness.CleanDecoderRate.agrees line 79
  16. theorem OAI.PerfectCompleteness.CleanDecoderRate.bound line 93
  17. theorem OAI.PerfectCompleteness.CleanDecoderRate.amplified_bound line 130
  18. abbrev OAI.PerfectCompleteness.CleanDecoderPairLaw.F2 line 159
  19. abbrev OAI.PerfectCompleteness.CleanDecoderPairLaw.context line 165
  20. abbrev OAI.PerfectCompleteness.CleanDecoderPairLaw.occurrences line 168
  21. abbrev OAI.PerfectCompleteness.CleanDecoderPairLaw.leftOwn line 171
  22. abbrev OAI.PerfectCompleteness.CleanDecoderPairLaw.rightOwn line 174
  23. abbrev OAI.PerfectCompleteness.CleanDecoderPairLaw.LeftAnswer line 177
  24. abbrev OAI.PerfectCompleteness.CleanDecoderPairLaw.RightAnswer line 180
  25. instance OAI.PerfectCompleteness.CleanDecoderPairLaw.leftAnswerFintype line 183
  26. instance OAI.PerfectCompleteness.CleanDecoderPairLaw.rightAnswerFintype line 187
  27. abbrev OAI.PerfectCompleteness.CleanDecoderPairLaw.Pair line 190
  28. instance OAI.PerfectCompleteness.CleanDecoderPairLaw.pairFintype line 192
  29. def OAI.PerfectCompleteness.CleanDecoderPairLaw.read line 195
  30. def OAI.PerfectCompleteness.CleanDecoderPairLaw.readSample line 199
  31. def OAI.PerfectCompleteness.CleanDecoderPairLaw.pairKernel line 213
  32. def OAI.PerfectCompleteness.CleanDecoderPairLaw.pairLaw line 218
  33. theorem OAI.PerfectCompleteness.CleanDecoderPairLaw.read_law line 223
  34. theorem OAI.PerfectCompleteness.CleanDecoderPairLaw.probability_read line 230
  35. theorem OAI.PerfectCompleteness.CleanDecoderPairLaw.law_pushforward line 244
  36. def OAI.PerfectCompleteness.CleanDecoderPairLaw.pairAgrees line 260
  37. theorem OAI.PerfectCompleteness.CleanDecoderPairLaw.pairAgrees_read line 269
  38. theorem OAI.PerfectCompleteness.CleanDecoderPairLaw.pair_probability_eq line 273
  39. theorem OAI.PerfectCompleteness.CleanDecoderPairLaw.bound line 280
  40. theorem OAI.PerfectCompleteness.CleanDecoderPairLaw.amplified_bound line 290