OAI/Combinatorics/SharpRamsey/Geometry/TotalDegreeCombination.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Incidence bounds for rich lines and finite point configurations.

  1. lemma OAI.SharpLogRamsey.CoprimeCombination.totalDegree_combination_le line 21
  2. abbrev OAI.SharpLogRamsey.NonplaneCertificate.Index line 34
  3. def OAI.SharpLogRamsey.NonplaneCertificate.flatFamily line 36
  4. lemma OAI.SharpLogRamsey.NonplaneCertificate.squarefree_equiv line 40
  5. lemma OAI.SharpLogRamsey.NonplaneCertificate.totalDegree_equiv_le line 48
  6. lemma OAI.SharpLogRamsey.NonplaneCertificate.pderiv_equiv line 51
  7. lemma OAI.SharpLogRamsey.NonplaneCertificate.nonplane_witness line 55
  8. lemma OAI.SharpLogRamsey.NonplaneCertificate.totalDegree_partial_le line 87
  9. lemma OAI.SharpLogRamsey.NonplaneCertificate.totalDegree_tangent_le line 93
  10. lemma OAI.SharpLogRamsey.NonplaneCertificate.totalDegree_flatness_le line 103
  11. lemma OAI.SharpLogRamsey.NonplaneCertificate.totalDegree_family_le line 117
  12. theorem OAI.SharpLogRamsey.NonplaneCertificate.exists_coprime_flat_combination line 122
  13. lemma OAI.SharpLogRamsey.LineFlatness.deriv_aeval line 140
  14. lemma OAI.SharpLogRamsey.LineFlatness.deriv2_aeval line 158
  15. def OAI.SharpLogRamsey.LineFlatness.restrictLine line 174
  16. lemma OAI.SharpLogRamsey.LineFlatness.eval_restrictLine line 178
  17. lemma OAI.SharpLogRamsey.LineFlatness.derivative_restrictLine line 185
  18. lemma OAI.SharpLogRamsey.LineFlatness.line_tangent line 192
  19. lemma OAI.SharpLogRamsey.LineFlatness.line_hessian line 198
  20. lemma OAI.SharpLogRamsey.LineFlatness.pderiv_swap line 214
  21. lemma OAI.SharpLogRamsey.LineFlatness.quadratic_vandermonde line 224
  22. theorem OAI.SharpLogRamsey.LineFlatness.binary_quadratic_three line 233
  23. def OAI.SharpLogRamsey.LineFlatness.hessian line 252
  24. lemma OAI.SharpLogRamsey.LineFlatness.hessian_smul_left line 256
  25. lemma OAI.SharpLogRamsey.LineFlatness.hessian_smul_right line 264
  26. lemma OAI.SharpLogRamsey.LineFlatness.hessian_add_left line 272
  27. lemma OAI.SharpLogRamsey.LineFlatness.hessian_add_right line 277
  28. lemma OAI.SharpLogRamsey.LineFlatness.hessian_symm line 281
  29. def OAI.SharpLogRamsey.LineFlatness.scaledTangent line 292
  30. lemma OAI.SharpLogRamsey.LineFlatness.tangent_expansion line 295
  31. lemma OAI.SharpLogRamsey.LineFlatness.tangent_projection_independent line 306
  32. lemma OAI.SharpLogRamsey.LineFlatness.tangent_projection_det line 327
  33. theorem OAI.SharpLogRamsey.LineFlatness.three_lines_flat line 338
  34. lemma OAI.SharpLogRamsey.LineFlatness.three_lines_all_tangents line 375
  35. lemma OAI.SharpLogRamsey.LineFlatness.hessian_rename line 399
  36. lemma OAI.SharpLogRamsey.LineFlatness.restrictLine_rename line 411
  37. lemma OAI.SharpLogRamsey.LineFlatness.tangent_rename line 416
  38. lemma OAI.SharpLogRamsey.LineFlatness.independent_rename line 425
  39. theorem OAI.SharpLogRamsey.LineFlatness.three_lines_tangent_zero line 434