OAI/Combinatorics/RamseyFive/Geometry/Q.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SharpRamseyFive.ProjectiveIncidence.sum_weightOnHyperplane_sq line 14
  2. lemma OAI.SharpRamseyFive.ProjectiveIncidence.sum_entry_column line 57
  3. def OAI.SharpRamseyFive.ProjectiveIncidence.Q line 65
  4. lemma OAI.SharpRamseyFive.ProjectiveIncidence.Q_pos line 67
  5. lemma OAI.SharpRamseyFive.ProjectiveIncidence.card_points line 73
  6. lemma OAI.SharpRamseyFive.ProjectiveIncidence.card_hyperplanes line 79
  7. theorem OAI.SharpRamseyFive.ProjectiveIncidence.incidence_mean line 85
  8. theorem OAI.SharpRamseyFive.ProjectiveIncidence.incidence_variance_eq line 94
  9. theorem OAI.SharpRamseyFive.ProjectiveIncidence.incidence_variance line 144
  10. theorem OAI.SharpRamseyFive.ProjectiveIncidence.incidence_weighted_mixing_sq line 153
  11. def OAI.SharpRamseyFive.ProjectiveIncidence.incidences line 177
  12. lemma OAI.SharpRamseyFive.ProjectiveIncidence.incidences_eq_sum line 181
  13. theorem OAI.SharpRamseyFive.ProjectiveIncidence.incidence_mixing line 186
  14. lemma OAI.SharpRamseyFive.ProjectiveIncidence.Q_recurrence line 207
  15. lemma OAI.SharpRamseyFive.ProjectiveIncidence.density_lower line 212
  16. theorem OAI.SharpRamseyFive.ProjectiveIncidence.sparse_rectangle_size line 225