OAI/Geometry/BallPacking/Moser/ManifoldMoserField.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PackingSufficiencySupport.Hamiltonian.ManifoldOneForm line 18
  2. def OAI.PackingSufficiencySupport.Hamiltonian.chartOneForm line 21
  3. def OAI.PackingSufficiencySupport.Hamiltonian.manifoldMoserField line 25
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartTwoForm_isInvertible line 29
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.chart_moser_contraction line 38
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeChartField_moser_eq line 58
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeChartField_moser_contDiffAt line 70
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.periodic_parameter_arg_smooth line 91
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.angularExtension_parameter_smooth line 106
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.angularExtension_parameter_compact line 131
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.circlePullback_parameter_smooth line 152
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_parametric_circle_primitive line 160
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.fiber_fderiv line 219
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.fiber_fderiv_smooth line 228
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.fiber_fderiv_compact line 238
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.parametric_finite_potential_correction line 250
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_parametric_finite_circle_correction line 298
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.fixedStep_affine line 327
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.stepEndpoint_affine line 354
  20. def OAI.PackingSufficiencySupport.Hamiltonian.parameterField line 367
  21. def OAI.PackingSufficiencySupport.Hamiltonian.fiberField line 370
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.parameterField_lipschitz line 375
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.fiberField_lipschitz line 383
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.parameterField_smooth line 391
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.fiberField_smooth line 395
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeStep_fiber line 399
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeSteps_fiber line 423
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeSteps_fiber_smooth line 438
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.fiberField_compact line 468
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_parametric_density_transport line 476