OAI/Geometry/BallPacking/Moser/PlanarCovectorPrimitive.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.Hamiltonian.planarCovector line 13
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarCovector_apply line 16
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarCovector_zero line 19
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarCovector_smooth line 22
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.planar_deriv_first line 27
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.planar_deriv_second line 33
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarCovector_exterior line 39
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.fixed_spatial_covector_primitive line 61
  9. def OAI.PackingSufficiencySupport.Hamiltonian.symplecticProjection line 93
  10. def OAI.PackingSufficiencySupport.Hamiltonian.symplecticNormalJet line 96
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.symplecticProjection_leftInverse line 100
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.symplecticProjection_pairing line 105
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.symplecticProjection_normal line 111
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.symplecticNormalJet_tangent line 116
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.symplecticNormalJet_normal line 122
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.corrected_moser_vector_tangent line 128
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.smooth_bilinear_flip line 152
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.symplecticProjection_contDiffAt line 166
  19. def OAI.PackingSufficiencySupport.Hamiltonian.staticPullbackOneForm line 184
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.staticPullbackOneForm_smoothAt line 187
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.staticPullbackOneForm_fderiv line 192
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.staticPullbackOneForm_exterior line 205
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.translated_covector_exterior line 226
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.translated_spatial_covector_primitive line 246
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.bilinearComp_isInvertible line 284
  26. abbrev OAI.PackingSufficiencySupport.Hamiltonian.ManifoldTwoForm line 300
  27. def OAI.PackingSufficiencySupport.Hamiltonian.preferredDifferential line 304
  28. def OAI.PackingSufficiencySupport.Hamiltonian.chartDifferential line 307
  29. def OAI.PackingSufficiencySupport.Hamiltonian.chartTwoForm line 310
  30. def OAI.PackingSufficiencySupport.Hamiltonian.timeChartField line 315
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartTwoForm_apply_chart line 320
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeChartField_hasDerivAt line 334
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.chart_spatial_pullback line 351
  34. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeChartField_contDiffOn line 399
  35. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldFamily_coordinate_smoothAt line 429
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeField_smooth_of_coordinates line 452