OAI/Geometry/BallPacking/SurfaceArea/AnnularSecondPositivity.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.globalSurfaceSecondPath_isInvertible_annular line 18
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.globalSurfaceSecondPath_isInvertible line 73
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.globalSurfaceSecondPath_moser_endpoint line 129
  4. def OAI.PackingSufficiencySupport.Hamiltonian.cylinderAreaCoefficient line 214
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderAreaCoefficient_periodic line 217
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderAreaCoefficient_rep line 230
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_cylinder_area_primitive line 251
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_annular_area_primitive line 287
  9. def OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.clockPrimitive line 338
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.clockPrimitive_smooth line 344
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.clockPrimitive_exterior line 352
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.clockPrimitive_eq line 364
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.exists_normal_form line 391
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.normalize_primitive line 450