OAI/Geometry/BallPacking/Annuli/CircleHandleBump.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.circle_oneForm_closed line 14
  2. def OAI.PackingSufficiencySupport.Hamiltonian.weightedCircleAngular line 27
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.weightedCircleAngular_chart line 29
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.weightedCircleAngular_smooth line 35
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.weightedCircleAngular_pullback line 51
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_normalized_circle_bump line 57
  7. abbrev OAI.PackingSufficiencySupport.Hamiltonian.TorusModel line 99
  8. abbrev OAI.PackingSufficiencySupport.Hamiltonian.HandleTorus line 100
  9. instance OAI.PackingSufficiencySupport.Hamiltonian.torus_chartedSpace line 102
  10. instance OAI.PackingSufficiencySupport.Hamiltonian.torus_manifold line 105
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.torus_snd_smooth line 110
  12. def OAI.PackingSufficiencySupport.Hamiltonian.torusHandleForm line 116
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.torusHandleForm_apply line 119
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.torusHandleForm_smooth line 126
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.torusHandleForm_closed line 141
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.torusHandleForm_support line 148
  17. def OAI.PackingSufficiencySupport.Hamiltonian.transverseTorusCircle line 161
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.transverseTorusCircle_smooth line 163
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.torusHandleForm_transverse line 170
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_torus_handle_form line 186
  21. abbrev OAI.PackingSufficiencySupport.Hamiltonian.CylinderModel line 207
  22. abbrev OAI.PackingSufficiencySupport.Hamiltonian.HandleCylinder line 208
  23. instance OAI.PackingSufficiencySupport.Hamiltonian.cylinder_chartedSpace line 210
  24. instance OAI.PackingSufficiencySupport.Hamiltonian.cylinder_manifold line 213
  25. def OAI.PackingSufficiencySupport.Hamiltonian.torusAnnulusMap line 218
  26. def OAI.PackingSufficiencySupport.Hamiltonian.torusAnnulusInverse line 219
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.torusAnnulusMap_smooth line 221
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.torusAnnulusInverse_smooth line 229
  29. def OAI.PackingSufficiencySupport.Hamiltonian.torusAnnulus line 240
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.torusAnnulus_compact line 261
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.torusAnnulus_pullback line 265
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.torusHandleForm_tsupport line 290
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinder_snd_smooth line 299
  34. def OAI.PackingSufficiencySupport.Hamiltonian.cylinderAngular line 305
  35. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderAngular_apply line 308
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderAngular_smooth line 315
  37. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderAngular_closed line 323
  38. def OAI.PackingSufficiencySupport.Hamiltonian.cylinderCover line 329
  39. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderCover_smooth line 331
  40. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderCover_derivative line 337
  41. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderAngular_cover line 360
  42. def OAI.PackingSufficiencySupport.Hamiltonian.weightedCylinderAngular line 366
  43. theorem OAI.PackingSufficiencySupport.Hamiltonian.weightedCylinderAngular_chart line 369
  44. theorem OAI.PackingSufficiencySupport.Hamiltonian.weightedCylinderAngular_smoothAt line 376
  45. theorem OAI.PackingSufficiencySupport.Hamiltonian.circleTurn_eq_iff line 396
  46. theorem OAI.PackingSufficiencySupport.Hamiltonian.periodic_eq_of_circleTurn_eq line 409
  47. def OAI.PackingSufficiencySupport.Hamiltonian.circlePeriodicDescent line 414
  48. theorem OAI.PackingSufficiencySupport.Hamiltonian.circlePeriodicDescent_turn line 417
  49. def OAI.PackingSufficiencySupport.Hamiltonian.localCircleLift line 421
  50. theorem OAI.PackingSufficiencySupport.Hamiltonian.circleTurn_add line 424
  51. theorem OAI.PackingSufficiencySupport.Hamiltonian.localCircleLift_turn line 427
  52. theorem OAI.PackingSufficiencySupport.Hamiltonian.localCircleLift_smooth_at line 431
  53. theorem OAI.PackingSufficiencySupport.Hamiltonian.circlePeriodicDescent_local line 439
  54. theorem OAI.PackingSufficiencySupport.Hamiltonian.circlePeriodicDescent_smooth line 444
  55. def OAI.PackingSufficiencySupport.Hamiltonian.circleFamilyDescent line 454
  56. theorem OAI.PackingSufficiencySupport.Hamiltonian.circleFamilyDescent_turn line 458
  57. theorem OAI.PackingSufficiencySupport.Hamiltonian.circleFamilyDescent_smoothOn line 463
  58. def OAI.PackingSufficiencySupport.Hamiltonian.stripPrimitive line 488
  59. def OAI.PackingSufficiencySupport.Hamiltonian.annularPrimitive line 491
  60. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularPrimitive_smooth line 494
  61. theorem OAI.PackingSufficiencySupport.Hamiltonian.stripPrimitive_smooth line 522