OAI/Computability/PerfectCompleteness/Foundations/DesignatedLeavesLemmas.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.DesignatedLeaves.selected line 20
  2. abbrev OAI.PerfectCompleteness.DesignatedLeaves.Children line 23
  3. abbrev OAI.PerfectCompleteness.DesignatedLeaves.Leaves line 24
  4. def OAI.PerfectCompleteness.DesignatedLeaves.equiv line 26
  5. theorem OAI.PerfectCompleteness.DesignatedLeaves.equiv_apply line 34
  6. theorem OAI.PerfectCompleteness.DesignatedLeaves.equiv_symm_apply line 37
  7. theorem OAI.PerfectCompleteness.DesignatedLeaves.card_leaves line 40
  8. def OAI.PerfectCompleteness.DesignatedLeaves.childStrategy line 50
  9. theorem OAI.PerfectCompleteness.DesignatedLeaves.wins_eq line 55
  10. theorem OAI.PerfectCompleteness.DesignatedLeaves.occurrence_law line 79
  11. theorem OAI.PerfectCompleteness.DesignatedLeaves.success_eq line 85
  12. theorem OAI.PerfectCompleteness.FiniteConditioningBounds.condition_probability_mono_on line 106
  13. theorem OAI.PerfectCompleteness.FiniteConditioningBounds.sum_record_inter line 118
  14. theorem OAI.PerfectCompleteness.FiniteConditioningBounds.sum_record_weight line 128
  15. theorem OAI.PerfectCompleteness.FiniteConditioningBounds.probability_le_record_bound line 139
  16. theorem OAI.PerfectCompleteness.FiniteConditioningBounds.conditioned_source_success line 161
  17. theorem OAI.PerfectCompleteness.FiniteConditioningBounds.independent_clean_bound line 184