OAI/Geometry/BallPacking/Forms/ManifoldFormTransport.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartOneForm_manifoldPullback_at line 20
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldPullbackOneForm_smooth_on line 34
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifold_pullback_exterior_on line 53
  4. def OAI.PackingSufficiencySupport.Hamiltonian.parameterEuclideanPullbackOneForm line 125
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.parameterEuclideanPullbackOneForm_contDiffAt line 129
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.euclidean_manifold_pullback_exterior_at line 163
  7. def OAI.PackingSufficiencySupport.Hamiltonian.parameterManifoldPullbackOneForm line 205
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.parameterManifoldPullback_chart_germ line 211
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.parameterManifoldPullbackOneForm_contDiffAt line 233
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifold_pullback_exterior_at line 259
  11. instance OAI.PackingSufficiencySupport.Hamiltonian.(instance at line 339) line 339
  12. instance OAI.PackingSufficiencySupport.Hamiltonian.(instance at line 342) line 342
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.flatProduct_fst_smooth line 348
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.flatProduct_snd_smooth line 354
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.flatProduct_fst_derivative line 360
  16. def OAI.PackingSufficiencySupport.Hamiltonian.productHorizontalLift line 366
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.productHorizontalLift_apply line 370
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.productHorizontalLift_vertical line 374
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.productHorizontalLift_chart line 381
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.productHorizontalLift_smooth line 397
  21. def OAI.PackingSufficiencySupport.Hamiltonian.flatProductMap line 429
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.flatProductMap_smoothAt line 432
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.flatProductMap_derivative line 440
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.productHorizontalLift_pullback_apply line 458
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.productHorizontalLift_exterior_pullback line 469
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.bilinearComp_equiv_isInvertible line 493
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.bilinearComp_equiv_isInvertible_iff line 504