OAI/Geometry/BallPacking/Flows/ManifoldFormTransport.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.Hamiltonian.manifoldPullback line 15
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifold_form_transport_derivative line 21
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifold_form_transport_constant line 85
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.local_manifold_form_transport_derivative line 99
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldMoserField_moment_tangent line 172
  6. def OAI.PackingSufficiencySupport.Hamiltonian.chartField line 198
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartField_smoothOn line 202
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartCurve_hasMFDerivAt line 214
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_global_bounded_trajectory line 244
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.stepEndpoint_eq_trajectory line 304
  11. def OAI.PackingSufficiencySupport.Hamiltonian.shortFlow line 323
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.shortFlow_zero line 326
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.shortFlow_smoothOn line 336
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.shortFlow_derivative line 345
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_smooth_local_manifold_flow line 370
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_smooth_local_manifold_family line 426
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_uniform_smooth_manifold_families line 462
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_global_compact_manifold_trajectory line 496