OAI/Geometry/BallPacking/Projective/SixLargeCubicPacking.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.CubicModel.actual_six_cubic_inner_polynomial_packing_avoid_axes_large line 15
  2. def OAI.PackingSufficiencySupport.CubicModel.quadricParam line 58
  3. def OAI.PackingSufficiencySupport.CubicModel.liftAlpha line 59
  4. def OAI.PackingSufficiencySupport.CubicModel.liftBeta line 60
  5. def OAI.PackingSufficiencySupport.CubicModel.liftGamma line 61
  6. def OAI.PackingSufficiencySupport.CubicModel.liftDelta line 62
  7. theorem OAI.PackingSufficiencySupport.CubicModel.lift_exponents line 64
  8. theorem OAI.PackingSufficiencySupport.CubicModel.lift_order_bounds line 72
  9. def OAI.PackingSufficiencySupport.CubicModel.quadricLiftMonomial line 79
  10. theorem OAI.PackingSufficiencySupport.CubicModel.quadricLiftMonomial_smooth line 82
  11. theorem OAI.PackingSufficiencySupport.CubicModel.quadricLiftMonomial_param line 87
  12. theorem OAI.PackingSufficiencySupport.CubicModel.quadricLiftMonomial_homogeneous line 100
  13. def OAI.PackingSufficiencySupport.CubicModel.quadricLiftPolynomial line 112
  14. theorem OAI.PackingSufficiencySupport.CubicModel.quadricLiftPolynomial_smooth line 115
  15. theorem OAI.PackingSufficiencySupport.CubicModel.quadricLiftPolynomial_param line 120
  16. theorem OAI.PackingSufficiencySupport.CubicModel.quadricLiftPolynomial_homogeneous line 130
  17. theorem OAI.PackingSufficiencySupport.CubicModel.quadricLiftPolynomial_orders line 141
  18. def OAI.PackingSufficiencySupport.CubicModel.planeCubicPolynomial line 155
  19. theorem OAI.PackingSufficiencySupport.CubicModel.planeCubicPolynomial_eval line 158
  20. theorem OAI.PackingSufficiencySupport.CubicModel.planeCubicPolynomial_degreeOf line 164
  21. theorem OAI.PackingSufficiencySupport.CubicModel.planeCubicPolynomial_totalDegree line 180
  22. def OAI.PackingSufficiencySupport.CubicModel.coefficientPowers line 197
  23. theorem OAI.PackingSufficiencySupport.CubicModel.coefficientPowers_bounds line 202
  24. def OAI.PackingSufficiencySupport.CubicModel.coefficientPolynomial line 212
  25. theorem OAI.PackingSufficiencySupport.CubicModel.coefficientPolynomial_eval line 215
  26. theorem OAI.PackingSufficiencySupport.CubicModel.coefficientPolynomial_degreeOf line 228
  27. theorem OAI.PackingSufficiencySupport.CubicModel.coefficientPolynomial_totalDegree line 237
  28. def OAI.PackingSufficiencySupport.CubicModel.cubicNormalSection line 244
  29. theorem OAI.PackingSufficiencySupport.CubicModel.cubicNormalSection_eval line 247
  30. theorem OAI.PackingSufficiencySupport.CubicModel.cubicNormalSection_degreeOf line 251
  31. theorem OAI.PackingSufficiencySupport.CubicModel.cubicNormalSection_totalDegree line 257
  32. theorem OAI.PackingSufficiencySupport.CubicModel.cubic_lift_integer_bounds line 263
  33. def OAI.PackingSufficiencySupport.CubicModel.firstQuadric line 270
  34. theorem OAI.PackingSufficiencySupport.CubicModel.firstQuadric_smooth line 272
  35. theorem OAI.PackingSufficiencySupport.CubicModel.firstQuadric_homogeneous line 276
  36. theorem OAI.PackingSufficiencySupport.CubicModel.inner_lattice_bounds line 281
  37. def OAI.PackingSufficiencySupport.CubicModel.liftedSection line 297
  38. theorem OAI.PackingSufficiencySupport.CubicModel.liftedSection_smooth line 303
  39. theorem OAI.PackingSufficiencySupport.CubicModel.liftedSection_homogeneous line 307
  40. theorem OAI.PackingSufficiencySupport.CubicModel.liftedSection_origin_orders line 322
  41. def OAI.PackingSufficiencySupport.CubicModel.firstQuadricChart line 338
  42. theorem OAI.PackingSufficiencySupport.CubicModel.firstQuadricChart_smooth line 340
  43. def OAI.PackingSufficiencySupport.CubicModel.outerTube line 349
  44. theorem OAI.PackingSufficiencySupport.CubicModel.outerTube_smooth line 352
  45. theorem OAI.PackingSufficiencySupport.CubicModel.outerTube_firstQuadric line 356
  46. def OAI.PackingSufficiencySupport.CubicModel.outerPolynomial line 362
  47. def OAI.PackingSufficiencySupport.CubicModel.outerConePolynomial line 367
  48. theorem OAI.PackingSufficiencySupport.CubicModel.outerPolynomial_smooth line 374
  49. theorem OAI.PackingSufficiencySupport.CubicModel.outerConePolynomial_smooth line 378
  50. theorem OAI.PackingSufficiencySupport.CubicModel.outerConePolynomial_eq line 386
  51. theorem OAI.PackingSufficiencySupport.CubicModel.outerConePolynomial_zero line 402
  52. theorem OAI.PackingSufficiencySupport.Hamiltonian.primitivePullback_comp line 425
  53. theorem OAI.PackingSufficiencySupport.CubicModel.quadricLiftPolynomial_one line 440
  54. theorem OAI.PackingSufficiencySupport.CubicModel.outerConePolynomial_vertex line 445
  55. theorem OAI.PackingSufficiencySupport.CubicModel.outerPolynomial_vertex line 451
  56. theorem OAI.PackingSufficiencySupport.CubicModel.outerConePolynomial_nonzero line 457
  57. theorem OAI.PackingSufficiencySupport.CubicModel.outerPolynomial_nonzero line 465
  58. def OAI.PackingSufficiencySupport.CubicModel.outerAmbientPrimitive line 473
  59. theorem OAI.PackingSufficiencySupport.CubicModel.outerAmbientPrimitive_smooth line 477
  60. def OAI.PackingSufficiencySupport.CubicModel.outerAmbientForm line 486
  61. def OAI.PackingSufficiencySupport.CubicModel.outerConePrimitive line 489
  62. theorem OAI.PackingSufficiencySupport.CubicModel.outerConePrimitive_smooth line 493
  63. theorem OAI.PackingSufficiencySupport.CubicModel.outerConePrimitive_zero line 516
  64. theorem OAI.PackingSufficiencySupport.CubicModel.outerConePrimitive_positive line 533
  65. theorem OAI.PackingSufficiencySupport.CubicModel.outerTube_isEmbedding line 551
  66. theorem OAI.PackingSufficiencySupport.CubicModel.exists_actual_outer_normal_transfer line 568