OAI/Geometry/BallPacking/CircleAction/DegreeCircleCovariance.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseDot_rotate line 15
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseArea_rotate line 21
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseCircleAction_differential line 27
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.degreeHopfDifference_rotate line 33
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.cutoffDegreePrimitive_rotate line 43
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.cutoffDegreeForm_circle_invariant line 52
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.cutoffDegreePrimitive_linear_pullback line 74
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.cutoffDegreeForm_subspace_nondegenerate line 88
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.euler_circle_curve_derivative line 128
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.euler_circle_untwisted_derivative line 136
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.euler_circle_equivariant line 151
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.splitInclusion_isSmoothEmbedding line 170
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_degree_relative_radial_moser line 189
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.diffeomorphicFormPullback_inverse line 244
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.radius_preserving_fderiv line 264
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.moment_pullback_generator line 275
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.circle_equivariant_on_radius line 306