OAI/Geometry/BallPacking/Flows/NonautonomousManifoldFlow.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_nonautonomous_manifold_flow line 16
  2. def OAI.PackingSufficiencySupport.Hamiltonian.nonautonomousSlice line 64
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_spatially_compact_nonautonomous_flow line 82
  4. theorem OAI.PackingSufficiencySupport.constant_above_on_convex line 136
  5. theorem OAI.PackingSufficiencySupport.sublevel_iff_of_zero_in_collar line 167
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifold_flow_sublevels_iff line 191
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifold_flow_image_sublevels line 227
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifold_relative_sublevel_moser line 254
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifold_exact_sublevel_moser line 353
  10. def OAI.PackingSufficiencySupport.Hamiltonian.PreservesTwoFormOn line 408
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.PreservesTwoFormOn.trans line 419
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.PreservesTwoFormOn.symm line 432
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifold_exact_moser_endpoint line 455
  14. def OAI.PackingSufficiencySupport.Hamiltonian.FormNeighborhoodEmbedding line 502
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.FormNeighborhoodEmbedding.transport line 509
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.transport_form_packing line 528
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.FormNeighborhoodEmbedding.postcompose line 555
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.postcompose_form_packing line 579
  19. def OAI.PackingSufficiencySupport.Hamiltonian.successorStandardForm line 601
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.successorStandardForm_apply line 604
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.isBallEmbedding_iff_formNeighborhoodEmbedding line 607