OAI/Combinatorics/SharpRamsey/Geometry/Triple.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Incidence bounds for rich lines and finite point configurations.

  1. abbrev OAI.SharpLogRamsey.PolynomialCoordinates.Triple line 16
  2. def OAI.SharpLogRamsey.PolynomialCoordinates.encode line 18
  3. lemma OAI.SharpLogRamsey.PolynomialCoordinates.encode_C line 23
  4. lemma OAI.SharpLogRamsey.PolynomialCoordinates.encode_X line 26
  5. lemma OAI.SharpLogRamsey.PolynomialCoordinates.encode_natDegree line 37
  6. lemma OAI.SharpLogRamsey.PolynomialCoordinates.coeff_degree_le line 43
  7. lemma OAI.SharpLogRamsey.PolynomialCoordinates.encode_coeff_natDegree line 49
  8. def OAI.SharpLogRamsey.PolynomialCoordinates.changeHom line 58
  9. def OAI.SharpLogRamsey.PolynomialCoordinates.unchangeHom line 60
  10. lemma OAI.SharpLogRamsey.PolynomialCoordinates.unchange_change line 63
  11. lemma OAI.SharpLogRamsey.PolynomialCoordinates.change_unchange line 72
  12. def OAI.SharpLogRamsey.PolynomialCoordinates.change line 82
  13. lemma OAI.SharpLogRamsey.PolynomialCoordinates.totalDegree_aeval_linear line 87
  14. lemma OAI.SharpLogRamsey.PolynomialCoordinates.change_degree line 107
  15. lemma OAI.SharpLogRamsey.PolynomialCoordinates.eval_change line 123
  16. lemma OAI.SharpLogRamsey.PolynomialCoordinates.eval_encode line 135
  17. lemma OAI.SharpLogRamsey.CommonLines.coprime_equiv line 156
  18. lemma OAI.SharpLogRamsey.CommonLines.eval_change_shear line 163
  19. lemma OAI.SharpLogRamsey.CommonLines.graph_zero line 170
  20. theorem OAI.SharpLogRamsey.CommonLines.card_le line 210
  21. def OAI.SharpLogRamsey.AffineIncidence.carrier line 261
  22. lemma OAI.SharpLogRamsey.AffineIncidence.parametrization_injective line 263
  23. lemma OAI.SharpLogRamsey.AffineIncidence.rebase line 268
  24. lemma OAI.SharpLogRamsey.AffineIncidence.scale line 282
  25. lemma OAI.SharpLogRamsey.AffineIncidence.independent_at_intersection line 292
  26. lemma OAI.SharpLogRamsey.AffineIncidence.intersection_subsingleton line 308
  27. lemma OAI.SharpLogRamsey.AffineIncidence.points_intersection_le line 325
  28. def OAI.SharpLogRamsey.AffineIncidence.pencil line 336
  29. def OAI.SharpLogRamsey.AffineIncidence.onLine line 339
  30. def OAI.SharpLogRamsey.AffineIncidence.richPoints line 342
  31. def OAI.SharpLogRamsey.AffineIncidence.poorPoints line 345
  32. lemma OAI.SharpLogRamsey.AffineIncidence.split_points line 349
  33. lemma OAI.SharpLogRamsey.AffineIncidence.poor_total line 355
  34. theorem OAI.SharpLogRamsey.AffineIncidence.pruning_bound line 380
  35. lemma OAI.SharpLogRamsey.NonplaneRichLines.eval_of_restrict_zero line 410
  36. lemma OAI.SharpLogRamsey.NonplaneRichLines.restrict_zero_rebase line 419
  37. lemma OAI.SharpLogRamsey.NonplaneRichLines.three_lines_at_rich line 431
  38. lemma OAI.SharpLogRamsey.NonplaneRichLines.many_parameters line 456