OAI/Computability/PerfectCompleteness/Foundations/ExactConditionalOutput.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.ExactConditionalOutput.enumeration line 16
  2. def OAI.PerfectCompleteness.ExactConditionalOutput.copies line 18
  3. theorem OAI.PerfectCompleteness.ExactConditionalOutput.copies_length line 22
  4. theorem OAI.PerfectCompleteness.ExactConditionalOutput.copies_filter_length line 27
  5. def OAI.PerfectCompleteness.ExactConditionalOutput.localOutput line 44
  6. def OAI.PerfectCompleteness.ExactConditionalOutput.output line 46
  7. theorem OAI.PerfectCompleteness.ExactConditionalOutput.localOutput_length line 48
  8. theorem OAI.PerfectCompleteness.ExactConditionalOutput.output_length line 52
  9. theorem OAI.PerfectCompleteness.ExactConditionalOutput.output_nonempty line 62
  10. def OAI.PerfectCompleteness.ExactConditionalOutput.localCount line 73
  11. theorem OAI.PerfectCompleteness.ExactConditionalOutput.localOutput_filter_length line 76
  12. theorem OAI.PerfectCompleteness.ExactConditionalOutput.output_filter_length line 82
  13. def OAI.PerfectCompleteness.ExactConditionalOutput.conditionalRate line 93
  14. def OAI.PerfectCompleteness.ExactConditionalOutput.average line 96
  15. theorem OAI.PerfectCompleteness.ExactConditionalOutput.localCount_div line 99
  16. theorem OAI.PerfectCompleteness.ExactConditionalOutput.conditionalRate_sum line 107
  17. theorem OAI.PerfectCompleteness.ExactConditionalOutput.rate_eq line 116
  18. theorem OAI.PerfectCompleteness.ExactConditionalOutput.output_support line 125
  19. def OAI.PerfectCompleteness.ExactConditionalOutput.construct line 139
  20. theorem OAI.PerfectCompleteness.ExactConditionalOutput.construct_length line 146
  21. theorem OAI.PerfectCompleteness.ExactConditionalOutput.count_eq line 151
  22. theorem OAI.PerfectCompleteness.ExactConditionalOutput.construct_rate_eq line 160
  23. theorem OAI.PerfectCompleteness.ExactConditionalOutput.value_le line 171
  24. theorem OAI.PerfectCompleteness.ExactConditionalOutput.perfectlyComplete line 182
  25. theorem OAI.PerfectCompleteness.ExactConditionalOutput.complete_value_eq_one line 194
  26. theorem OAI.PerfectCompleteness.ExactConditionalOutput.conditionalRate_uniformization line 204