OAI/Geometry/NearbyLagrangian/HamiltonianFlow.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Flat time changes and compact Hamiltonian trajectories.

  1. lemma OAI.NearbyLagrangian.Transport.smoothTime_mem line 19
  2. lemma OAI.NearbyLagrangian.Transport.contDiff_flat_time line 22
  3. lemma OAI.NearbyLagrangian.Transport.smoothTime_deriv_zero line 28
  4. def OAI.NearbyLagrangian.Transport.flatTimeField line 41
  5. lemma OAI.NearbyLagrangian.Transport.contDiff_flatTimeField line 44
  6. lemma OAI.NearbyLagrangian.Transport.compactSupport_flatTimeField line 53
  7. lemma OAI.NearbyLagrangian.Transport.flatTime_solution line 67
  8. lemma OAI.NearbyLagrangian.Transport.compact_map_bounds line 76
  9. def OAI.NearbyLagrangian.Transport.symplecticGradient line 96
  10. lemma OAI.NearbyLagrangian.Transport.symplecticGradient_zero line 100
  11. lemma OAI.NearbyLagrangian.Transport.symplecticGradient_identity line 103
  12. lemma OAI.NearbyLagrangian.Transport.contDiff_symplecticGradient line 115
  13. def OAI.NearbyLagrangian.Transport.phaseDifferential line 121
  14. def OAI.NearbyLagrangian.Transport.hamiltonianField line 124
  15. lemma OAI.NearbyLagrangian.Transport.phaseDifferential_eq line 128
  16. lemma OAI.NearbyLagrangian.Transport.contDiff_hamiltonianField line 133
  17. lemma OAI.NearbyLagrangian.Transport.hamiltonianField_identity line 141
  18. lemma OAI.NearbyLagrangian.Transport.hamiltonianField_support line 145
  19. lemma OAI.NearbyLagrangian.Transport.compactSupport_hamiltonianField line 159
  20. lemma OAI.NearbyLagrangian.Transport.symplecticGradient_smul line 177
  21. lemma OAI.NearbyLagrangian.Transport.contDiff_hamiltonian_slice line 182
  22. lemma OAI.NearbyLagrangian.Transport.flatHamiltonian_field line 187
  23. lemma OAI.NearbyLagrangian.Transport.flatHamiltonian_support line 196
  24. lemma OAI.NearbyLagrangian.Transport.flatHamiltonian_regular line 207
  25. def OAI.NearbyLagrangian.Transport.hamiltonianTrajectory line 224
  26. lemma OAI.NearbyLagrangian.Transport.contDiff_hamiltonianTrajectory line 228
  27. lemma OAI.NearbyLagrangian.Transport.hamiltonianTrajectory_initial line 235
  28. lemma OAI.NearbyLagrangian.Transport.hamiltonianTrajectory_velocity line 239
  29. lemma OAI.NearbyLagrangian.Transport.hamiltonianTrajectory_identity line 249
  30. theorem OAI.NearbyLagrangian.Transport.exists_flat_hamiltonian_evolution line 260