OAI/Geometry/UnitDistances/Basic.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PlanarUnitDistances.Plane line 7

    Also declared: ComparatorChallenges/PlanarUnitDistances.lean:7 (same declaration text).

  2. def OAI.PlanarUnitDistances.IsUnitPair line 9

    Also declared: ComparatorChallenges/PlanarUnitDistances.lean:9 (same declaration text).

  3. def OAI.PlanarUnitDistances.unitPairCount line 12

    Also declared: ComparatorChallenges/PlanarUnitDistances.lean:12 (same declaration text).

  4. def OAI.PlanarUnitDistances.u line 16

    Also declared: ComparatorChallenges/PlanarUnitDistances.lean:16 (same declaration text).

  5. def OAI.PlanarUnitDistances.MainClaim line 19
  6. theorem OAI.PlanarUnitDistances.isUnitPair_mk line 22
  7. theorem OAI.PlanarUnitDistances.not_isUnitPair_diag line 25
  8. theorem OAI.PlanarUnitDistances.unitPairCount_le_card_sq line 29
  9. theorem OAI.PlanarUnitDistances.attainable_nonempty line 39
  10. theorem OAI.PlanarUnitDistances.attainable_bddAbove line 44
  11. theorem OAI.PlanarUnitDistances.exists_maximizer line 50
  12. theorem OAI.PlanarUnitDistances.unitPairCount_le_u line 54
  13. theorem OAI.PlanarUnitDistances.u_le_sq line 57
  14. theorem OAI.PlanarUnitDistances.u_zero line 62
  15. theorem OAI.PlanarUnitDistances.unitPairCount_singleton line 64
  16. theorem OAI.PlanarUnitDistances.u_one line 68
  17. theorem OAI.PlanarUnitDistances.mainClaim_iff_uniform line 73
  18. theorem OAI.PlanarUnitDistances.arbitrarily_large_counterexample line 85
  19. theorem OAI.PlanarUnitDistances.counterexample_sequence line 119
  20. lemma OAI.PlanarUnitDistances.AlgebraicSpecialization.signs_in_nhds line 141
  21. theorem OAI.PlanarUnitDistances.AlgebraicSpecialization.dense_parameter_root line 158
  22. abbrev OAI.PlanarUnitDistances.AlgebraicSpecialization.ParameterPolynomial line 191
  23. def OAI.PlanarUnitDistances.AlgebraicSpecialization.evaluate line 193
  24. lemma OAI.PlanarUnitDistances.AlgebraicSpecialization.continuous_parameter_eval line 197
  25. theorem OAI.PlanarUnitDistances.AlgebraicSpecialization.rational_simple_root line 213
  26. lemma OAI.PlanarUnitDistances.AlgebraicSpecialization.evaluate_rat line 239
  27. lemma OAI.PlanarUnitDistances.AlgebraicSpecialization.algebraic_polynomial_value line 246
  28. lemma OAI.PlanarUnitDistances.AlgebraicSpecialization.algebraic_parameter_value line 253
  29. def OAI.PlanarUnitDistances.AlgebraicSpecialization.chartValue line 259
  30. theorem OAI.PlanarUnitDistances.AlgebraicSpecialization.specialize_chart line 262
  31. theorem OAI.PlanarUnitDistances.PrimitiveChart.finite_coordinates_primitive line 318
  32. theorem OAI.PlanarUnitDistances.PrimitiveChart.clear_polynomial line 349
  33. theorem OAI.PlanarUnitDistances.PrimitiveChart.clear_relation line 367
  34. abbrev OAI.PlanarUnitDistances.PrimitiveChart.ParameterField line 387
  35. def OAI.PlanarUnitDistances.PrimitiveChart.parameterMap line 390
  36. theorem OAI.PlanarUnitDistances.PrimitiveChart.coe_parameterMap line 395
  37. theorem OAI.PlanarUnitDistances.PrimitiveChart.parameterMap_injective line 405
  38. theorem OAI.PlanarUnitDistances.PrimitiveChart.parameterMap_fraction line 411
  39. theorem OAI.PlanarUnitDistances.PrimitiveChart.cleared_minpoly line 433
  40. lemma OAI.PlanarUnitDistances.PrimitiveChart.evaluate_as_map line 472
  41. theorem OAI.PlanarUnitDistances.PrimitiveChart.coordinate_polynomials line 479
  42. lemma OAI.PlanarUnitDistances.PrimitiveChart.cleared_unit_equation line 533
  43. def OAI.PlanarUnitDistances.PrimitiveChart.unitRelation line 545
  44. def OAI.PlanarUnitDistances.PrimitiveChart.unitEquation line 551
  45. lemma OAI.PlanarUnitDistances.PrimitiveChart.evaluate_unitRelation line 554
  46. theorem OAI.PlanarUnitDistances.PrimitiveChart.algebraic_unit_approximation line 561
  47. lemma OAI.PlanarUnitDistances.PrimitiveChart.plane_dist_sq line 604
  48. lemma OAI.PlanarUnitDistances.PrimitiveChart.plane_unit_iff line 609
  49. lemma OAI.PlanarUnitDistances.PrimitiveChart.plane_close_of_coordinates line 617
  50. lemma OAI.PlanarUnitDistances.PrimitiveChart.finite_separation line 626
  51. theorem OAI.PlanarUnitDistances.PrimitiveChart.algebraic_planar_specialization line 644
  52. theorem OAI.PlanarUnitDistances.unitPairCount_map_mono line 679
  53. theorem OAI.PlanarUnitDistances.algebraic_set_specialization line 691
  54. theorem OAI.PlanarUnitDistances.mainClaim_iff_algebraic line 711
  55. theorem OAI.PlanarUnitDistances.algebraic_counterexample_sequence line 726