OAI/Combinatorics/SharpRamsey/Geometry/Weight.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Incidence bounds for rich lines and finite point configurations.

  1. def OAI.SharpLogRamsey.Sampling.weight line 16
  2. def OAI.SharpLogRamsey.Sampling.selected line 19
  3. theorem OAI.SharpLogRamsey.Sampling.mem_selected line 22
  4. theorem OAI.SharpLogRamsey.Sampling.weight_nonneg line 26
  5. theorem OAI.SharpLogRamsey.Sampling.sum_weight line 32
  6. theorem OAI.SharpLogRamsey.Sampling.containment_moment line 37
  7. def OAI.SharpLogRamsey.Sampling.count line 66
  8. theorem OAI.SharpLogRamsey.Sampling.family_moment line 69
  9. theorem OAI.SharpLogRamsey.Sampling.size_moment line 80
  10. theorem OAI.SharpLogRamsey.Sampling.exists_ge_mean line 90
  11. lemma OAI.SharpLogRamsey.RichSampling.moment line 108
  12. lemma OAI.SharpLogRamsey.RichSampling.exp_neg_half_le line 128
  13. lemma OAI.SharpLogRamsey.RichSampling.lower_tail line 134
  14. theorem OAI.SharpLogRamsey.RichSampling.exists_sample line 169
  15. abbrev OAI.SharpLogRamsey.Interpolation.Box line 235
  16. def OAI.SharpLogRamsey.Interpolation.exponent line 236
  17. lemma OAI.SharpLogRamsey.Interpolation.exponent_injective line 239
  18. lemma OAI.SharpLogRamsey.Interpolation.exponent_degree_le line 244
  19. lemma OAI.SharpLogRamsey.Interpolation.monomials_independent line 255
  20. theorem OAI.SharpLogRamsey.Interpolation.exists_vanishing line 259
  21. lemma OAI.SharpLogRamsey.SamplePolynomial.degree_le_of_dvd line 295
  22. lemma OAI.SharpLogRamsey.SamplePolynomial.squarefree_reduction line 305
  23. theorem OAI.SharpLogRamsey.SamplePolynomial.exists_polynomial line 319
  24. theorem OAI.SharpLogRamsey.RichAffineLines.card_mul_le line 381