OAI/Combinatorics/RamseyFive/Geometry/LargeCells.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpRamseyFive.ProjectiveTraining.chosen_shape_ne_of_positive_cell line 17
  2. def OAI.SharpRamseyFive.ProjectiveTraining.largeCells line 31
  3. lemma OAI.SharpRamseyFive.ProjectiveTraining.largeCells_card_budget line 34
  4. lemma OAI.SharpRamseyFive.ProjectiveTraining.earlier_mem_largeCells line 47
  5. def OAI.SharpRamseyFive.ProjectiveTraining.largeCellIntersections line 54
  6. lemma OAI.SharpRamseyFive.ProjectiveTraining.hyperplane_intersection_cap line 60
  7. lemma OAI.SharpRamseyFive.ProjectiveTraining.largeCellIntersections_card line 79
  8. theorem OAI.SharpRamseyFive.ProjectiveTraining.largeCellIntersections_budget line 103
  9. lemma OAI.SharpRamseyFive.ProjectiveTraining.surviving_large_plane_center_mem line 121
  10. lemma OAI.SharpRamseyFive.ProjectiveTraining.cellRichPlanes_variance line 136
  11. theorem OAI.SharpRamseyFive.ProjectiveTraining.weighted_small_cell_rich_planes line 161
  12. lemma OAI.SharpRamseyFive.ProjectiveTraining.earliest_plane_cell_rich line 195
  13. def OAI.SharpRamseyFive.ProjectiveTraining.headPlaneCenters line 211
  14. theorem OAI.SharpRamseyFive.ProjectiveTraining.head_center_plane_count line 217
  15. lemma OAI.SharpRamseyFive.ProjectiveTraining.actual_tail_hyperplane_cap line 293
  16. theorem OAI.SharpRamseyFive.ProjectiveTraining.actual_tail_rich_plane_exceptions line 301