OAI/Combinatorics/SharpRamsey/Geometry/RichLines.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Incidence bounds for rich lines and finite point configurations.

  1. theorem OAI.SharpLogRamsey.ImplicitBranch.hensel_nonmonic line 32
  2. lemma OAI.SharpLogRamsey.ImplicitBranch.aeval_hom line 124
  3. def OAI.SharpLogRamsey.ImplicitBranch.liftZ line 131
  4. lemma OAI.SharpLogRamsey.ImplicitBranch.eval_liftZ line 137
  5. lemma OAI.SharpLogRamsey.ImplicitBranch.derivative_liftZ line 145
  6. lemma OAI.SharpLogRamsey.ImplicitBranch.zeroCoeff_aeval line 155
  7. theorem OAI.SharpLogRamsey.ImplicitBranch.exists_formal_branch line 171
  8. lemma OAI.SharpLogRamsey.FlatnessCore.cast_ne_zero_of_lt line 214
  9. lemma OAI.SharpLogRamsey.FlatnessCore.coeff_deriv_predecessor line 219
  10. lemma OAI.SharpLogRamsey.FlatnessCore.degree_pos_coordinate line 232
  11. lemma OAI.SharpLogRamsey.FlatnessCore.coordinate_le_degree line 239
  12. theorem OAI.SharpLogRamsey.FlatnessCore.coeff_zero_of_hessian_zero line 247
  13. def OAI.SharpLogRamsey.FlatnessCore.jetIdeal line 275
  14. lemma OAI.SharpLogRamsey.FlatnessCore.mem_jetIdeal_iff line 285
  15. theorem OAI.SharpLogRamsey.FlatnessCore.hessian_zero_affine_jet line 293
  16. lemma OAI.SharpLogRamsey.FlatnessCore.aeval_sub_mem line 306
  17. lemma OAI.SharpLogRamsey.FlatnessCore.totalDegree_aeval_linear line 323
  18. lemma OAI.SharpLogRamsey.FlatnessCore.toSeries_aeval line 344
  19. lemma OAI.SharpLogRamsey.FlatnessCore.polynomial_eq_zero_of_jet line 354
  20. theorem OAI.SharpLogRamsey.FlatnessCore.flat_branch_zero_plane line 364
  21. lemma OAI.SharpLogRamsey.FlatnessCore.deriv_aeval line 391
  22. lemma OAI.SharpLogRamsey.FlatnessCore.deriv2_aeval line 409
  23. def OAI.SharpLogRamsey.FlatnessCore.branchPoint line 425
  24. def OAI.SharpLogRamsey.FlatnessCore.branchTangent line 428
  25. lemma OAI.SharpLogRamsey.FlatnessCore.branch_second_sum line 431