OAI/Geometry/BallPacking/Forms/ManifoldMapDifferential.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.Hamiltonian.manifoldMapDifferential line 20
  2. def OAI.PackingSufficiencySupport.Hamiltonian.manifoldPullbackTwoForm line 31
  3. def OAI.PackingSufficiencySupport.Hamiltonian.manifoldPullbackOneForm line 36
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartTwoForm_manifoldPullback line 42
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartOneForm_manifoldPullback line 57
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldPullbackTwoForm_smooth line 70
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldPullbackOneForm_smooth line 85
  8. def OAI.PackingSufficiencySupport.Hamiltonian.manifoldExteriorOneForm line 106
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartOneForm_transition line 110
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartOneForm_exterior_transition line 122
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldExteriorOneForm_chart line 154
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.euclidean_manifold_pullback_germ line 186
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.euclidean_manifold_pullback_chart_exterior line 198
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.euclidean_manifold_pullback_exterior line 218
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifold_pullback_exterior line 243
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.vector_chartOneForm line 305
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.vector_chartTwoForm line 311
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.vector_exteriorOneForm line 319
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.vector_oneForm_smooth line 329
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.vector_twoForm_smooth line 335
  21. def OAI.PackingSufficiencySupport.DiagonalQuadrics.phaseInclusion line 350
  22. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.phaseInclusion_smooth line 352
  23. def OAI.PackingSufficiencySupport.DiagonalQuadrics.curveFSPrimitive line 356
  24. def OAI.PackingSufficiencySupport.DiagonalQuadrics.curveFSForm line 359
  25. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveFSPrimitive_smooth line 362
  26. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveFSForm_smooth line 372
  27. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveFSPrimitive_exterior line 384
  28. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveFSForm_skew line 399
  29. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.phase_chart_function line 403
  30. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.realChart_complex_target line 412
  31. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.phase_chart_derivative line 419
  32. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveFSForm_positive line 433