OAI/Geometry/BallPacking/Annuli/AnnularHandleCurvature.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.annularCoverDomain line 15
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.annularCoverDomain_open line 20
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.annularCover_pullback_smoothAt line 25
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.annularCover_coefficients_smooth line 37
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.annularCover_curl line 50
  6. def OAI.PackingSufficiencySupport.Hamiltonian.handleAnnularCover line 85
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.handleAnnularCover_smoothAt line 89
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.handleAnnularCover_derivative line 96
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalHandleForm_cover line 105
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalHandleRadialForm_annular line 118
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalHandleRadialForm_cover line 143
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.handleAnnularCover_inverse line 157
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderCover_derivative_bijective line 168
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.handleAnnularCover_derivative_bijective line 182
  15. def OAI.PackingSufficiencySupport.Hamiltonian.handleAnnularCoverLinearEquiv line 208
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.handleAnnularCoverLinearEquiv_apply line 215
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.handleAnnularCover_derivative_bijective line 230
  18. def OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.handleAnnularCoverLinearEquiv line 256
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.handleAnnularCoverLinearEquiv_apply line 263
  20. def OAI.PackingSufficiencySupport.Hamiltonian.parameterEuclideanPullbackTwoForm line 279
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.parameterEuclideanPullbackTwoForm_contDiffAt line 284
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartTwoForm_manifoldPullback_at line 315
  23. def OAI.PackingSufficiencySupport.Hamiltonian.parameterManifoldPullbackTwoForm line 329
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.parameterManifoldPullbackTwoForm_chart_germ line 335
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.parameterManifoldPullbackTwoForm_contDiffAt line 357
  26. def OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.annularCoverTwoCoefficient line 392
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.annularCoverDomain_eq line 398
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.annularCoverTwoCoefficient_smooth line 405
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.annularCoverTwoCoefficient_ne_zero line 417
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.annularCoverTwoCoefficient_positive line 448
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.annularCover_positive_exterior line 482
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.handleAnnularCover_surjOn line 503