OAI/Geometry/BallPacking/Flows/AnnularPathGerms.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.annular_normalForm_cover line 19
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.globalSurfaceFirstPrimitive_cover_germ line 30
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.globalSurfaceSecondPrimitive_cover_germ line 51
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.globalSurfaceSecondEndpoint_cover_pullback line 81
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.globalSurfaceSecondEndpoint_shear_cover line 104
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.annularUnshearMap_pullback line 142
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_joint_localized_manifold_moser_field line 201
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.local_contraction_derivative line 286
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.local_moser_transport_equation line 300
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.joint_manifold_moser_PDE line 323
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.smoothAt_fderiv_apply_const line 381
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.local_spatial_fderiv line 391
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.local_time_fderiv line 398
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.local_flow_variation line 406
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.local_flow_form_derivative line 437