OAI/Geometry/BallPacking/Hopf/SixLargeQuadricPacking.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.CubicModel.actual_six_quadric_polynomial_packing_large line 13
  2. def OAI.PackingSufficiencySupport.Hamiltonian.radialSymplectization line 81
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialSymplectization_apply line 85
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialSymplectization_nondegenerate line 92
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialSymplectization_circle line 150
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialSymplectization_moser_tangent line 157
  7. def OAI.PackingSufficiencySupport.Hamiltonian.mixedHopfPrimitive line 166
  8. def OAI.PackingSufficiencySupport.Hamiltonian.mixedHopfForm line 170
  9. def OAI.PackingSufficiencySupport.Hamiltonian.homogeneousConePrimitive line 173
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.mixedHopfPrimitive_smoothAt line 177
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.mixedHopfForm_eq line 183
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.mixedHopfPrimitive_circle line 194
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.mixedHopfForm_radial line 203
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.mixedHopfForm_circle line 211
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.mixedHopfForm_skew line 219
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.mixedHopfForm_horizontal_positive line 224
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.homogeneousConePrimitive_exterior line 240
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.homogeneousConePrimitive_nondegenerate line 253
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.homogeneousConePrimitive_circle_contraction line 271
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.homogeneousConePrimitive_smoothAt line 280
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.homogeneousConePrimitive_affine line 285
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.homogeneousConePrimitive_circle line 294
  23. def OAI.PackingSufficiencySupport.Hamiltonian.hopfCurvaturePullback line 302
  24. def OAI.PackingSufficiencySupport.Hamiltonian.mixedHopfCurvaturePullback line 307
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.mixedHopfCurvaturePullback_gauge line 312
  26. def OAI.PackingSufficiencySupport.Hamiltonian.cartesianConjugate line 336
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.cartesianConjugate_smooth line 339
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.cartesianConjugate_cartesian line 343
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.mixedHopfCurvaturePullback_eq line 347
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.homogeneousDegree_euler line 378
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.cartesianConjugate_fderiv line 391
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.cartesianConjugate_euler line 399
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.cartesianConjugate_J line 407
  34. theorem OAI.PackingSufficiencySupport.Hamiltonian.cartesianConjugate_nonzero line 415
  35. def OAI.PackingSufficiencySupport.Hamiltonian.homogeneousVeronese line 427
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.homogeneousVeronese_smooth line 430
  37. theorem OAI.PackingSufficiencySupport.Hamiltonian.homogeneousVeronese_homogeneous line 437
  38. theorem OAI.PackingSufficiencySupport.Hamiltonian.homogeneousVeronese_nonzero line 443
  39. theorem OAI.PackingSufficiencySupport.Hamiltonian.homogeneousVeronese_sq line 453
  40. def OAI.PackingSufficiencySupport.Hamiltonian.veroneseRegularization line 460
  41. theorem OAI.PackingSufficiencySupport.Hamiltonian.veroneseRegularization_smooth line 464
  42. theorem OAI.PackingSufficiencySupport.Hamiltonian.veroneseRegularization_joint_smooth line 472
  43. theorem OAI.PackingSufficiencySupport.Hamiltonian.veroneseRegularization_homogeneous line 482
  44. theorem OAI.PackingSufficiencySupport.Hamiltonian.veroneseRegularization_nonzero line 493