OAI/Geometry/NearbyLagrangian/SupportedEvolution.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Compactly supported Hamiltonian evolution and its smooth motion.

  1. lemma OAI.NearbyLagrangian.Transport.mem_open_iff_of_fixed_outside line 19
  2. def OAI.NearbyLagrangian.Transport.restrictSupportedDiffeomorph line 30
  3. def OAI.NearbyLagrangian.Transport.openEvolution line 55
  4. lemma OAI.NearbyLagrangian.Transport.openEvolution_apply line 62
  5. lemma OAI.NearbyLagrangian.Transport.contMDiff_openEvolution line 69
  6. def OAI.NearbyLagrangian.Transport.chartEvolution line 89
  7. lemma OAI.NearbyLagrangian.Transport.chartEvolution_identity line 96
  8. lemma OAI.NearbyLagrangian.Transport.chartEvolution_initial line 106
  9. lemma OAI.NearbyLagrangian.Transport.contMDiff_chartEvolution line 116
  10. theorem OAI.NearbyLagrangian.Transport.exists_compact_hamiltonian_evolution line 132
  11. lemma OAI.NearbyLagrangian.Transport.hamiltonian_evolution_equation line 151
  12. structure OAI.NearbyLagrangian.Transport.SupportedHamiltonianEvolution line 169
  13. theorem OAI.NearbyLagrangian.Transport.exists_supportedHamiltonianEvolution line 180
  14. lemma OAI.NearbyLagrangian.Transport.SupportedHamiltonianEvolution.fixed line 188
  15. def OAI.NearbyLagrangian.Transport.SupportedHamiltonianEvolution.motion line 199
  16. lemma OAI.NearbyLagrangian.Transport.SupportedHamiltonianEvolution.motion_identity line 204
  17. lemma OAI.NearbyLagrangian.Transport.SupportedHamiltonianEvolution.motion_initial line 211
  18. lemma OAI.NearbyLagrangian.Transport.SupportedHamiltonianEvolution.motion_smooth line 217
  19. lemma OAI.NearbyLagrangian.Transport.contMDiff_timeSlice line 223
  20. lemma OAI.NearbyLagrangian.Transport.SupportedHamiltonianEvolution.motion_curve_smooth line 228
  21. lemma OAI.NearbyLagrangian.Transport.SupportedHamiltonianEvolution.motion_equation line 234