OAI/Geometry/NearbyLagrangian/GeneratingAction.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Liouville action identities and compact mixed generating functions.

  1. def OAI.NearbyLagrangian.Transport.euclideanLiouville line 19
  2. lemma OAI.NearbyLagrangian.Transport.euclideanLiouville_apply line 22
  3. def OAI.NearbyLagrangian.Transport.mixedSigma line 25
  4. lemma OAI.NearbyLagrangian.Transport.mixed_inverse_snd line 29
  5. lemma OAI.NearbyLagrangian.Transport.mixed_inverse_fst line 35
  6. lemma OAI.NearbyLagrangian.Transport.contDiff_mixedSigma line 40
  7. theorem OAI.NearbyLagrangian.Transport.hasFDerivAt_mixedSigma line 44
  8. theorem OAI.NearbyLagrangian.Transport.hasCompactSupport_mixedSigma line 72
  9. lemma OAI.NearbyLagrangian.Transport.hasFDerivAt_fderiv_apply_const line 101
  10. def OAI.NearbyLagrangian.Transport.flowVelocity line 111
  11. def OAI.NearbyLagrangian.Transport.actionIntegrand line 114
  12. lemma OAI.NearbyLagrangian.Transport.contDiff_actionIntegrand line 118
  13. theorem OAI.NearbyLagrangian.Transport.cartan_action_identity line 125
  14. theorem OAI.NearbyLagrangian.Transport.hasDerivAt_pullbackLiouvilleEval line 157
  15. theorem OAI.NearbyLagrangian.Transport.hasFDerivAt_intervalIntegral_contDiff line 184
  16. def OAI.NearbyLagrangian.Transport.flowLiouville line 218
  17. lemma OAI.NearbyLagrangian.Transport.flowLiouville_apply line 221
  18. lemma OAI.NearbyLagrangian.Transport.contDiff_flowLiouville line 224
  19. def OAI.NearbyLagrangian.Transport.hamiltonianAction line 229
  20. theorem OAI.NearbyLagrangian.Transport.hasFDerivAt_hamiltonianAction line 234
  21. theorem OAI.NearbyLagrangian.Transport.contDiff_hamiltonianAction line 263
  22. lemma OAI.NearbyLagrangian.Transport.flowVelocity_eq_zero_of_stationary line 279
  23. theorem OAI.NearbyLagrangian.Transport.hasCompactSupport_hamiltonianAction line 291
  24. lemma OAI.NearbyLagrangian.Transport.flowLiouville_slice line 314
  25. lemma OAI.NearbyLagrangian.Transport.flowLiouville_initial line 324
  26. theorem OAI.NearbyLagrangian.Transport.hasFDerivAt_hamiltonianAction_initial line 333
  27. theorem OAI.NearbyLagrangian.Transport.exists_compact_mixed_generating_function line 345