OAI/Combinatorics/RamseyFive/Geometry/HighGeometryClosure.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpRamseyFive.ProjectiveIncidence.RadialLine.exists_other line 15
  2. lemma OAI.SharpRamseyFive.ProjectiveIncidence.radial_card_le_points line 33
  3. lemma OAI.SharpRamseyFive.ProjectiveIncidence.geometric_card_le line 46
  4. lemma OAI.SharpRamseyFive.ProjectiveIncidence.projective_card_le_two_pow line 58
  5. lemma OAI.SharpRamseyFive.ProjectiveIncidence.center_radial_count_le line 64
  6. lemma OAI.SharpRamseyFive.ScoreGeometry.high_density_bounds line 86
  7. lemma OAI.SharpRamseyFive.ScoreGeometry.captured_cutoff line 114
  8. theorem OAI.SharpRamseyFive.ScoreGeometry.score_pair_captured_moment_sharp line 150
  9. theorem OAI.SharpRamseyFive.ScoreGeometry.score_pair_residual_moment_sharp line 189
  10. theorem OAI.SharpRamseyFive.ScoreGeometry.captured_global_trunc_exp_bound line 233
  11. theorem OAI.SharpRamseyFive.ScoreGeometry.residual_global_trunc_exp_bound_dim line 285