OAI/Geometry/BallPacking/CircleAction/CircleRelativeOneForm.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.differential_intertwine line 22
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.averageOneForm_apply line 38
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.averageOneForm_normal_annihilation line 48
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.symplecticHorizontalLift_unique line 89
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.horizontalSystem_contDiffAt line 100
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.symplecticHorizontalLift_contDiffAt line 123
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.vertical_nondegenerate_change line 140
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.symplecticHorizontalLift_change line 160
  9. def OAI.PackingSufficiencySupport.Hamiltonian.manifoldBaseDifferential line 183
  10. def OAI.PackingSufficiencySupport.Hamiltonian.manifoldBaseChart line 186
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldBaseChart_contDiffAt line 189
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.chart_fderiv_of_hasFDerivAt line 197
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldBaseChart_fderiv line 200
  14. def OAI.PackingSufficiencySupport.Hamiltonian.manifoldHorizontalField line 214
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.chart_horizontalField line 220
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldHorizontalField_smooth line 236
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifold_isLocallyConstant_of_differential_zero line 279
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifold_difference_constant line 305
  19. def OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.generator line 328
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.generator_natural line 331
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.equivariant_moment_difference_constant line 350
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.equivariant_moment_normalized line 374
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.vector_smooth line 399
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.averageOneForm_spatialDifferential line 404
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.averaged_spatial_differential_generator_zero line 422
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.differential_generator line 444
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.averageOneForm_generator_zero line 452
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.averageOneForm_add line 466
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.averaged_corrected_generator_zero line 476