OAI/Computability/PerfectCompleteness/Repetition/CleanPhysicalHighAverage.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.CleanPhysicalHighAverage.mpr_heq line 18
  2. abbrev OAI.PerfectCompleteness.CleanPhysicalHighAverage.suffix line 27
  3. theorem OAI.PerfectCompleteness.CleanPhysicalHighAverage.suffix_proper line 31
  4. abbrev OAI.PerfectCompleteness.CleanPhysicalHighAverage.nativeDirection line 45
  5. def OAI.PerfectCompleteness.CleanPhysicalHighAverage.tapeStatistic line 48
  6. def OAI.PerfectCompleteness.CleanPhysicalHighAverage.childStatistic line 66
  7. theorem OAI.PerfectCompleteness.CleanPhysicalHighAverage.childStatistic_congr line 74
  8. theorem OAI.PerfectCompleteness.CleanPhysicalHighAverage.rightInput_eq line 91
  9. theorem OAI.PerfectCompleteness.CleanPhysicalHighAverage.physical_probability_eq line 112
  10. def OAI.PerfectCompleteness.CleanPhysicalHighAverage.sourceStatistic line 136
  11. def OAI.PerfectCompleteness.CleanPhysicalHighAverage.questionStatistic line 147
  12. theorem OAI.PerfectCompleteness.CleanPhysicalHighAverage.sourceStatistic_eq_question line 158
  13. theorem OAI.PerfectCompleteness.CleanPhysicalHighAverage.physical_probability_eq_observed line 176
  14. theorem OAI.PerfectCompleteness.CleanPhysicalHighAverage.questionStatistic_expectation line 200
  15. theorem OAI.PerfectCompleteness.CleanPhysicalHighAverage.mean_probability_eq line 220
  16. theorem OAI.PerfectCompleteness.CleanPhysicalHighAverage.probability_eq_tag_average line 257