OAI/Combinatorics/SharpRamsey/Geometry/HessianTangent.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Incidence bounds for rich lines and finite point configurations.

  1. lemma OAI.SharpLogRamsey.FlatnessCore.hessian_zero_of_tangent_zero line 17
  2. def OAI.SharpLogRamsey.FlatnessCore.scaledTangent line 32
  3. def OAI.SharpLogRamsey.FlatnessCore.flatnessPolynomial line 35
  4. lemma OAI.SharpLogRamsey.FlatnessCore.aeval_scaledTangent line 42
  5. lemma OAI.SharpLogRamsey.FlatnessCore.first_branch_derivative line 50
  6. lemma OAI.SharpLogRamsey.FlatnessCore.scaled_branch_tangent line 59
  7. lemma OAI.SharpLogRamsey.FlatnessCore.flatness_root_implies_hessian_zero line 75
  8. lemma OAI.SharpLogRamsey.LocalFlatness.branch_constantCoeff line 107
  9. lemma OAI.SharpLogRamsey.LocalFlatness.rename_aeval line 117
  10. lemma OAI.SharpLogRamsey.LocalFlatness.plane_factor_of_zero line 130
  11. theorem OAI.SharpLogRamsey.LocalFlatness.exists_plane_factor_of_flatness line 144
  12. lemma OAI.SharpLogRamsey.PolynomialGeometry.totalDegree_pderiv_lt line 187
  13. lemma OAI.SharpLogRamsey.PolynomialGeometry.not_dvd_pderiv line 204
  14. lemma OAI.SharpLogRamsey.PolynomialGeometry.not_dvd_squarefree_derivative line 210
  15. lemma OAI.SharpLogRamsey.PolynomialGeometry.totalDegree_pos_of_irreducible line 226
  16. lemma OAI.SharpLogRamsey.PolynomialGeometry.exists_nonzero_pderiv line 234
  17. lemma OAI.SharpLogRamsey.PolynomialGeometry.exists_zero_not_zero line 268
  18. lemma OAI.SharpLogRamsey.PolynomialGeometry.exists_nonsingular_factor_zero line 283
  19. def OAI.SharpLogRamsey.Translation.translate line 296
  20. lemma OAI.SharpLogRamsey.Translation.translate_X line 300
  21. lemma OAI.SharpLogRamsey.Translation.translate_C line 302
  22. lemma OAI.SharpLogRamsey.Translation.pderiv_translate line 305
  23. lemma OAI.SharpLogRamsey.Translation.constantCoeff_translate line 317
  24. lemma OAI.SharpLogRamsey.Translation.translate_neg_translate line 324
  25. lemma OAI.SharpLogRamsey.Translation.translate_translate_neg line 331
  26. lemma OAI.SharpLogRamsey.Translation.translate_injective line 335
  27. lemma OAI.SharpLogRamsey.Translation.translate_dvd_iff line 338
  28. lemma OAI.SharpLogRamsey.Translation.translate_nonunit line 345
  29. lemma OAI.SharpLogRamsey.GlobalFlatness.totalDegree_translate_le line 356
  30. lemma OAI.SharpLogRamsey.GlobalFlatness.translate_flatness line 364
  31. theorem OAI.SharpLogRamsey.GlobalFlatness.plane_factor_of_flatness line 379
  32. lemma OAI.SharpLogRamsey.GlobalFlatness.nonplane_factor_not_flat line 409
  33. def OAI.SharpLogRamsey.CoprimeCombination.combinationMap line 425
  34. lemma OAI.SharpLogRamsey.CoprimeCombination.combinationMap_apply line 430
  35. theorem OAI.SharpLogRamsey.CoprimeCombination.exists_coprime_combination line 433