OAI/Computability/PerfectCompleteness/Reduction/FixedCallBudgetLemmas.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.FixedCallBudget.pairCount line 15
  2. def OAI.PerfectCompleteness.FixedCallBudget.budget line 18
  3. theorem OAI.PerfectCompleteness.FixedCallBudget.budget_pos line 22
  4. theorem OAI.PerfectCompleteness.FixedCallBudget.pairCount_le line 27
  5. theorem OAI.PerfectCompleteness.FixedCallBudget.original_calls_le line 45
  6. theorem OAI.PerfectCompleteness.FixedCallBudget.modified_calls_le line 54
  7. theorem OAI.PerfectCompleteness.FixedCallBudget.copied_calls_le line 63
  8. theorem OAI.PerfectCompleteness.FixedCallBudget.child_bound_mono line 69
  9. theorem OAI.PerfectCompleteness.FixedCallBudget.copied_calls_with_extra_le line 78
  10. def OAI.PerfectCompleteness.FixedParameters.calls line 95
  11. structure OAI.PerfectCompleteness.FixedParameters.Parameters line 98
  12. theorem OAI.PerfectCompleteness.FixedParameters.exists_parameters line 117
  13. def OAI.PerfectCompleteness.FixedParameters.branch line 139
  14. def OAI.PerfectCompleteness.FixedParameters.projectionProbability line 140
  15. theorem OAI.PerfectCompleteness.FixedParameters.branch_pos line 142
  16. theorem OAI.PerfectCompleteness.FixedParameters.projectionProbability_bounds line 147
  17. theorem OAI.PerfectCompleteness.FixedParameters.source_rate line 151