OAI/Geometry/BallPacking/Toric/ToricClosedShift.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.Hamiltonian.toricClosedShift line 16
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricClosedShift_smooth line 21
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricClosedShift_exterior line 28
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.globalSurfaceFirstPrimitive_isInvertible_outside line 58
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.globalSurfaceSecondPrimitive_isInvertible_outside line 76
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.globalSurfaceFirstPath_isInvertible line 110
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceSuspensionCoefficient_collarInvariant line 159
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceFirstCorrectionCoefficient_collarInvariant line 168
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceSecondExtraCoefficient_collarInvariant line 176
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalSurfaceFirstPrimitive_collarInvariant line 202
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalSurfaceSecondPrimitive_collarInvariant line 222
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.globalSurfaceFirstPrimitive_collarInvariant line 258
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.globalSurfaceSecondPrimitive_collarInvariant line 278
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.globalSurfaceFirstPath_moser_endpoint line 306