OAI/Combinatorics/SharpRamsey/Geometry/ScaledTangentDot.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Incidence bounds for rich lines and finite point configurations.

  1. lemma OAI.SharpLogRamsey.RichLinePolynomial.scaled_tangent_dot line 24
  2. lemma OAI.SharpLogRamsey.RichLinePolynomial.eval_flatness line 28
  3. theorem OAI.SharpLogRamsey.RichLinePolynomial.family_zero_at_three_lines line 45
  4. lemma OAI.SharpLogRamsey.RichLinePolynomial.natDegree_aeval_linear line 85
  5. lemma OAI.SharpLogRamsey.RichLinePolynomial.restriction_degree line 105
  6. lemma OAI.SharpLogRamsey.RichLinePolynomial.restriction_eval line 113
  7. lemma OAI.SharpLogRamsey.RichLinePolynomial.restriction_zero_of_many line 121
  8. theorem OAI.SharpLogRamsey.RichLinePolynomial.auxiliary_polynomial line 132
  9. lemma OAI.SharpLogRamsey.ParametricBezout.isCoprime_map_fraction line 169
  10. lemma OAI.SharpLogRamsey.ParametricBezout.resultant_ne_zero_of_isRelPrime line 200
  11. lemma OAI.SharpLogRamsey.ParametricBezout.natDegree_det_le line 213
  12. lemma OAI.SharpLogRamsey.ParametricBezout.resultant_degree_bound line 228
  13. lemma OAI.SharpLogRamsey.ParametricBezout.resultant_eval_zero line 248
  14. lemma OAI.SharpLogRamsey.ParametricBezout.common_points_card_le line 257
  15. lemma OAI.SharpLogRamsey.ParametricBezout.no_common_point_of_degree_zero line 280
  16. theorem OAI.SharpLogRamsey.ParametricBezout.graph_branches_card_le line 302
  17. lemma OAI.SharpLogRamsey.GenericCoordinates.exists_eval_ne_zero line 334
  18. lemma OAI.SharpLogRamsey.GenericCoordinates.exists_first line 340
  19. lemma OAI.SharpLogRamsey.GenericCoordinates.exists_second line 362
  20. def OAI.SharpLogRamsey.GenericCoordinates.shear line 385
  21. abbrev OAI.SharpLogRamsey.GenericCoordinates.first line 393
  22. lemma OAI.SharpLogRamsey.GenericCoordinates.first_apply line 397
  23. def OAI.SharpLogRamsey.GenericCoordinates.line line 399
  24. def OAI.SharpLogRamsey.GenericCoordinates.direction line 400
  25. def OAI.SharpLogRamsey.GenericCoordinates.base line 401
  26. lemma OAI.SharpLogRamsey.GenericCoordinates.map_direction line 405
  27. lemma OAI.SharpLogRamsey.GenericCoordinates.map_base line 408
  28. lemma OAI.SharpLogRamsey.GenericCoordinates.line_normalize line 412
  29. theorem OAI.SharpLogRamsey.GenericCoordinates.exists_separating_coordinates line 428