OAI/Geometry/BallPacking/RelativeJets/SymplecticProjectionNaturality.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.symplecticProjection_natural line 18
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.normal_annihilation_pullback line 33
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.moser_vector_tangent_of_annihilation line 44
  4. def OAI.PackingSufficiencySupport.Hamiltonian.localNormalJet line 60
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.localNormalJet_contDiffOn line 62
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.localNormalJet_zero line 67
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.localNormalJet_hasFDerivAt line 71
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.product_normal_first_jet line 82
  9. def OAI.PackingSufficiencySupport.Hamiltonian.splitInclusion line 107
  10. def OAI.PackingSufficiencySupport.Hamiltonian.splitRetraction line 110
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.splitRetraction_eq line 113
  12. def OAI.PackingSufficiencySupport.Hamiltonian.localSymplecticPotential line 118
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.localSymplecticPotential_zero line 122
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.symplecticNormalJet_contDiffAt line 129
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.localSymplecticPotential_contDiffAt line 137
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.localSymplecticPotential_hasFDerivAt line 145
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.maximalChart_inverse_differential line 176
  18. def OAI.PackingSufficiencySupport.Hamiltonian.maximalChartLinearEquiv line 207
  19. def OAI.PackingSufficiencySupport.Hamiltonian.relativeLocalPotential line 220
  20. def OAI.PackingSufficiencySupport.Hamiltonian.relativeLocalDomain line 225
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.relativeLocalDomain_isOpen line 232
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.relativeLocalPotential_contMDiffOn line 253
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.symplecticProjection_reparametrize line 281
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.symplecticNormalJet_reparametrize line 295
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.symplecticProjection_changeCoordinates line 305
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.symplecticNormalJet_changeCoordinates line 320
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.adapted_restriction_isInvertible line 335
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.adapted_normal_jet line 352
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.fderiv_eq_of_hasFDerivAt line 380
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.adapted_inclusion_differential line 385
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.maximalChart_pullback_two line 421
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.maximalChart_pullback_one line 432
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.relativeLocalDomain_mem line 443
  34. theorem OAI.PackingSufficiencySupport.Hamiltonian.relativeLocalPotential_hasMFDerivAt line 462