OAI/Geometry/UnitDistances/Loci.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarUnitDistances.LocusAvoidance.zeros line 10
  2. lemma OAI.PlanarUnitDistances.LocusAvoidance.zeros_subset line 13
  3. lemma OAI.PlanarUnitDistances.LocusAvoidance.zeros_one line 16
  4. lemma OAI.PlanarUnitDistances.LocusAvoidance.zeros_unit line 19
  5. theorem OAI.PlanarUnitDistances.LocusAvoidance.exists_maximizer line 26
  6. lemma OAI.PlanarUnitDistances.LocusAvoidance.size_X line 42
  7. theorem OAI.PlanarUnitDistances.LocusAvoidance.exists_factor_witness line 45
  8. theorem OAI.PlanarUnitDistances.LocusAvoidance.plane_or_curve line 55
  9. lemma OAI.PlanarUnitDistances.LocusAvoidance.eval_swap line 93
  10. lemma OAI.PlanarUnitDistances.LocusAvoidance.zeros_swap line 98
  11. lemma OAI.PlanarUnitDistances.LocusAvoidance.size_swap line 102
  12. lemma OAI.PlanarUnitDistances.LocusAvoidance.zeros_card_le_of_degree_zero line 105
  13. lemma OAI.PlanarUnitDistances.LocusAvoidance.both_degrees_pos_of_many_zeros line 128
  14. theorem OAI.PlanarUnitDistances.LocusAvoidance.eventually_both_degrees_pos line 142
  15. lemma OAI.PlanarUnitDistances.PlaneIntersection.resultant_ne_zero_of_irreducible line 161
  16. lemma OAI.PlanarUnitDistances.PlaneIntersection.eval_resultant_zero line 179
  17. lemma OAI.PlanarUnitDistances.PlaneIntersection.natDegree_det_le line 187
  18. lemma OAI.PlanarUnitDistances.PlaneIntersection.natDegree_resultant_le line 204
  19. theorem OAI.PlanarUnitDistances.PlaneIntersection.intersection_card_le line 216
  20. lemma OAI.PlanarUnitDistances.RealCurveSymmetry.coeff_degree_le_swap_degree line 241
  21. lemma OAI.PlanarUnitDistances.RealCurveSymmetry.degree_le_size line 247
  22. lemma OAI.PlanarUnitDistances.RealCurveSymmetry.coeff_degree_le_size line 250
  23. def OAI.PlanarUnitDistances.RealCurveSymmetry.conjugate line 254
  24. def OAI.PlanarUnitDistances.RealCurveSymmetry.reflect line 257
  25. lemma OAI.PlanarUnitDistances.RealCurveSymmetry.conjugate_injective line 259
  26. lemma OAI.PlanarUnitDistances.RealCurveSymmetry.conjugate_degree line 262
  27. lemma OAI.PlanarUnitDistances.RealCurveSymmetry.swap_conjugate line 265
  28. lemma OAI.PlanarUnitDistances.RealCurveSymmetry.reflect_size line 269
  29. lemma OAI.PlanarUnitDistances.RealCurveSymmetry.reflect_degree line 274
  30. lemma OAI.PlanarUnitDistances.RealCurveSymmetry.reflect_ne_zero line 277
  31. lemma OAI.PlanarUnitDistances.RealCurveSymmetry.reflect_eval line 282
  32. theorem OAI.PlanarUnitDistances.RealCurveSymmetry.reflect_eq_const_mul line 288
  33. lemma OAI.PlanarUnitDistances.RealCurveSymmetry.projection_degrees_eq line 317
  34. abbrev OAI.PlanarUnitDistances.UltraCurve.CU line 330
  35. lemma OAI.PlanarUnitDistances.UltraCurve.eval_mk line 332
  36. lemma OAI.PlanarUnitDistances.UltraCurve.swap_bimapping line 342
  37. def OAI.PlanarUnitDistances.UltraCurve.locus line 352
  38. lemma OAI.PlanarUnitDistances.UltraCurve.pack_eq line 355
  39. lemma OAI.PlanarUnitDistances.UltraCurve.locus_irreducible line 361
  40. lemma OAI.PlanarUnitDistances.UltraCurve.locus_root line 367
  41. lemma OAI.PlanarUnitDistances.UltraCurve.locus_degrees line 375
  42. def OAI.PlanarUnitDistances.CirclePolynomial.circle line 413
  43. lemma OAI.PlanarUnitDistances.CirclePolynomial.eval_circle line 416
  44. lemma OAI.PlanarUnitDistances.CirclePolynomial.circle_ne_zero line 421
  45. lemma OAI.PlanarUnitDistances.CirclePolynomial.circle_degree line 426
  46. lemma OAI.PlanarUnitDistances.CirclePolynomial.swap_circle line 439
  47. lemma OAI.PlanarUnitDistances.CirclePolynomial.circle_size line 444
  48. theorem OAI.PlanarUnitDistances.CirclePolynomial.eq_mul_const line 447
  49. theorem OAI.PlanarUnitDistances.ComplexCircle.centers_conjugate line 474
  50. lemma OAI.PlanarUnitDistances.UltraCircle.eventual_equation line 513
  51. lemma OAI.PlanarUnitDistances.UltraCircle.mk_circle_iff line 529
  52. lemma OAI.PlanarUnitDistances.UltraCircle.real_circle_iff line 536
  53. theorem OAI.PlanarUnitDistances.UltraCircle.forbidden line 549