OAI/Geometry/BallPacking/Moser/SymplecticFamily.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.Hamiltonian.familyGenerator line 15
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.familyGenerator_smooth line 18
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.fderiv_apply_const line 24
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.family_symplectic_variation line 34
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.familyGenerator_fderiv_image line 67
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.family_fderiv_right_inverse line 92
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.familyGenerator_infinitesimal line 107
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.familyGenerator_support line 135
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_hamiltonian_of_symplectic_family line 157
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeStep_preserves_form line 212
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeSteps_preserves_form line 285
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_form_transport line 309
  13. def OAI.PackingSufficiencySupport.Hamiltonian.formMoserField line 344
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.formMoserField_smooth line 347
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.formMoserField_solve line 357
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.formMoserField_support line 363
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.formMoserField_contraction_derivative line 371
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.formMoserField_transport_equation line 388
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.formMoserField_tangent line 409
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_compact_form_moser line 423
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeStep_comp_smooth line 458
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeSteps_variable_smooth line 472
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeStep_zero line 492
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeSteps_zero line 501
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.fixedStep_eq_solution line 513
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeStep_eq_solution line 535
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeSteps_eq_solution line 563
  28. def OAI.PackingSufficiencySupport.Hamiltonian.spatialDifferential line 584
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.spatialDifferential_apply line 587
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.spatialDifferential_smooth line 590
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.spatialDifferential_support line 594
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.spatialDifferential_fderiv line 600
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.spatialDifferential_closed line 612
  34. def OAI.PackingSufficiencySupport.Hamiltonian.hamiltonianField line 623
  35. theorem OAI.PackingSufficiencySupport.Hamiltonian.hamiltonianField_smooth line 628
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.hamiltonianField_contraction line 634
  37. theorem OAI.PackingSufficiencySupport.Hamiltonian.hamiltonianField_support line 640
  38. theorem OAI.PackingSufficiencySupport.Hamiltonian.hamiltonianField_transport_equation line 644
  39. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_hamiltonian_endpoint line 659