OAI/Combinatorics/RamseyFive/Entropy/Tail.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpRamseyFive.HighPlaneBudget.tail line 18
  2. def OAI.SharpRamseyFive.HighPlaneBudget.tailPlanes line 22
  3. def OAI.SharpRamseyFive.HighPlaneBudget.headAt line 25
  4. def OAI.SharpRamseyFive.HighPlaneBudget.richAt line 29
  5. lemma OAI.SharpRamseyFive.HighPlaneBudget.rich_planes_split line 34
  6. lemma OAI.SharpRamseyFive.HighPlaneBudget.head_degree_sum line 69
  7. theorem OAI.SharpRamseyFive.HighPlaneBudget.head_exceptions line 86
  8. theorem OAI.SharpRamseyFive.HighPlaneBudget.rich_count_outside_exceptions line 109
  9. theorem OAI.SharpRamseyFive.HighPlaneBudget.tail_exceptions line 138
  10. def OAI.SharpRamseyFive.HighPlaneBudget.capturedPairs line 160
  11. theorem OAI.SharpRamseyFive.HighPlaneBudget.captured_pair_count line 165
  12. theorem OAI.SharpRamseyFive.HighPlaneBudget.captured_pairs_outside_exceptions line 185