OAI/Geometry/BallPacking/Forms/SpatialOneForm.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.spatialDifferential_contDiffAt line 13
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.spatialDifferential_fderivAt line 17
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.spatialDifferential_closedAt line 29
  4. def OAI.PackingSufficiencySupport.Hamiltonian.manifoldSpatialDifferential line 48
  5. def OAI.PackingSufficiencySupport.Hamiltonian.manifoldPotentialChart line 51
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldPotentialChart_contDiffAt line 54
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartDifferential_inverse line 63
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartOneForm_manifoldSpatialDifferential line 73
  9. def OAI.PackingSufficiencySupport.Hamiltonian.euclideanPullbackTwoForm line 107
  10. def OAI.PackingSufficiencySupport.Hamiltonian.euclideanPullbackOneForm line 112
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.euclideanPullbackTwoForm_chart line 116
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.euclideanPullbackOneForm_chart line 135
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.euclideanPullbackTwoForm_contDiffAt line 161
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.euclideanPullbackOneForm_contDiffAt line 188
  15. def OAI.PackingSufficiencySupport.Hamiltonian.chartSupportedOneForm line 225
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartSupportedOneForm_chart line 230
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartSupportedOneForm_zero line 251
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartSupportedOneForm_compact line 266
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartSupportedOneForm_smooth line 273
  20. def OAI.PackingSufficiencySupport.Hamiltonian.chartSupportedTwoForm line 316
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartSupportedTwoForm_chart line 321
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartSupportedTwoForm_zero line 343
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartSupportedTwoForm_compact line 358
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartSupportedTwoForm_smooth line 365
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.euclideanExteriorOneForm_zero_outside line 415
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartSupportedOneForm_exterior line 429
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.chart_supported_area_primitive line 496
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.chart_primitive_support_compact line 535