OAI/Geometry/NearbyLagrangian/Isotopies.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Reversal, flattening and uniform bounds for compact Hamiltonian isotopies.

  1. lemma OAI.NearbyLagrangian.antisymmetric_CLM_neg_left line 17
  2. lemma OAI.NearbyLagrangian.symplecticForm_neg_left line 23
  3. def OAI.NearbyLagrangian.reverseIsotopy line 28
  4. def OAI.NearbyLagrangian.reverseHamiltonian line 31
  5. lemma OAI.NearbyLagrangian.reverseTime_mem line 34
  6. lemma OAI.NearbyLagrangian.reverseTimeDerivative line 37
  7. lemma OAI.NearbyLagrangian.reverseCurveDerivative line 49
  8. lemma OAI.NearbyLagrangian.scalarDerivative_neg line 66
  9. lemma OAI.NearbyLagrangian.reverseIsotopy_velocity line 72
  10. theorem OAI.NearbyLagrangian.IsCompactHamiltonianIsotopy.reverse line 86
  11. theorem OAI.NearbyLagrangian.reverseIsotopy_range_endpoint line 121
  12. lemma OAI.NearbyLagrangian.antisymmetric_CLM_smul_left line 151
  13. lemma OAI.NearbyLagrangian.symplecticForm_smul_left line 158
  14. lemma OAI.NearbyLagrangian.smoothCurveDerivative line 168
  15. lemma OAI.NearbyLagrangian.scalarDerivative_const_mul line 186
  16. lemma OAI.NearbyLagrangian.timeSlice_mdifferentiable line 193
  17. def OAI.NearbyLagrangian.flattenIsotopy line 201
  18. def OAI.NearbyLagrangian.flattenHamiltonian line 204
  19. lemma OAI.NearbyLagrangian.contMDiff_flattenIsotopy line 207
  20. lemma OAI.NearbyLagrangian.contMDiff_flattenHamiltonian line 216
  21. lemma OAI.NearbyLagrangian.flattenIsotopy_velocity line 228
  22. theorem OAI.NearbyLagrangian.IsCompactHamiltonianIsotopy.flatten_equation line 240
  23. lemma OAI.NearbyLagrangian.flattenIsotopy_zero line 269
  24. lemma OAI.NearbyLagrangian.flattenIsotopy_one line 273
  25. theorem OAI.NearbyLagrangian.IsCompactHamiltonianIsotopy.flatten line 277
  26. lemma OAI.NearbyLagrangian.compact_support_param_bound line 304
  27. theorem OAI.NearbyLagrangian.IsCompactHamiltonianIsotopy.uniform_bound line 321