OAI/Combinatorics/SharpRamsey/Geometry/VectorMap.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Incidence bounds for rich lines and finite point configurations.

  1. def OAI.SharpLogRamsey.ProjectiveBaseChange.vectorMap line 14
  2. lemma OAI.SharpLogRamsey.ProjectiveBaseChange.vectorMap_apply line 19
  3. lemma OAI.SharpLogRamsey.ProjectiveBaseChange.vectorMap_injective line 22
  4. def OAI.SharpLogRamsey.ProjectiveBaseChange.vectorSemi line 27
  5. lemma OAI.SharpLogRamsey.ProjectiveBaseChange.vectorSemi_apply line 32
  6. lemma OAI.SharpLogRamsey.ProjectiveBaseChange.vectorSemi_injective line 35
  7. def OAI.SharpLogRamsey.ProjectiveBaseChange.pointMap line 38
  8. lemma OAI.SharpLogRamsey.ProjectiveBaseChange.pointMap_injective line 41
  9. lemma OAI.SharpLogRamsey.ProjectiveBaseChange.coordinate_decomposition line 60
  10. def OAI.SharpLogRamsey.ProjectiveBaseChange.extendDual line 65
  11. lemma OAI.SharpLogRamsey.ProjectiveBaseChange.extendDual_map line 68
  12. def OAI.SharpLogRamsey.ProjectiveBaseChange.extendSpace line 80
  13. theorem OAI.SharpLogRamsey.ProjectiveBaseChange.mem_extendSpace line 83
  14. theorem OAI.SharpLogRamsey.ProjectiveBaseChange.rational_hyperplane line 104
  15. def OAI.SharpLogRamsey.ProjectiveAffineChart.first line 143
  16. lemma OAI.SharpLogRamsey.ProjectiveAffineChart.first_apply line 146
  17. def OAI.SharpLogRamsey.ProjectiveAffineChart.lift line 149
  18. lemma OAI.SharpLogRamsey.ProjectiveAffineChart.lift_zero line 152
  19. lemma OAI.SharpLogRamsey.ProjectiveAffineChart.lift_succ line 153
  20. lemma OAI.SharpLogRamsey.ProjectiveAffineChart.first_lift line 154
  21. lemma OAI.SharpLogRamsey.ProjectiveAffineChart.lift_ne_zero line 158
  22. def OAI.SharpLogRamsey.ProjectiveAffineChart.chart line 164
  23. lemma OAI.SharpLogRamsey.ProjectiveAffineChart.normalize_eq_lift line 167
  24. lemma OAI.SharpLogRamsey.ProjectiveAffineChart.mk_lift_chart line 185
  25. lemma OAI.SharpLogRamsey.ProjectiveAffineChart.chart_injOn line 194
  26. lemma OAI.SharpLogRamsey.ProjectiveAffineChart.lift_mem_iff line 201
  27. theorem OAI.SharpLogRamsey.ProjectiveAffineChart.lift_mem_span_pair line 208
  28. theorem OAI.SharpLogRamsey.ProjectiveAffineChart.exists_avoiding line 245
  29. theorem OAI.SharpLogRamsey.AffinePlaneCoefficients.degree_one_form line 287
  30. lemma OAI.SharpLogRamsey.AffinePlaneCoefficients.eval_degree_one line 320
  31. lemma OAI.SharpLogRamsey.RationalAffineChart.map_submodule line 339
  32. lemma OAI.SharpLogRamsey.RationalAffineChart.map_submodule_le line 345
  33. abbrev OAI.SharpLogRamsey.RationalAffineChart.coord line 351
  34. def OAI.SharpLogRamsey.RationalAffineChart.Avoids line 354
  35. lemma OAI.SharpLogRamsey.RationalAffineChart.coord_injOn line 357
  36. lemma OAI.SharpLogRamsey.RationalAffineChart.lift_coord_mem line 362
  37. lemma OAI.SharpLogRamsey.RationalAffineChart.lift_coord_kernel line 367
  38. lemma OAI.SharpLogRamsey.RationalAffineChart.exists_avoiding line 373
  39. def OAI.SharpLogRamsey.RationalAffineChart.homogeneousPlane line 379
  40. lemma OAI.SharpLogRamsey.RationalAffineChart.homogeneousPlane_lift line 384
  41. lemma OAI.SharpLogRamsey.RationalAffineChart.homogeneousPlane_ne_zero line 390
  42. theorem OAI.SharpLogRamsey.RationalAffineChart.plane_cap_transfer line 401
  43. lemma OAI.SharpLogRamsey.ProjectiveLineChart.extendSpace_span_pair line 436