OAI/Geometry/BallPacking/CircleAction/CircleRelativeRadialMoser.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_circle_relative_radial_moser line 18
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.cutoffDegreePrimitive_smooth_family line 94
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.cutoffDegreePrimitive_moser_data line 102
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.cutoffDegreePrimitive_circle_contraction line 124
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.cutoffDegreePrimitive_time_circle line 137
  6. def OAI.PackingSufficiencySupport.Hamiltonian.phaseShell line 155
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseShell_isCompact line 157
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseShell_nonzero line 176
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseShell_radial line 185
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_global_homogeneous_cone_path line 191
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.homogeneous_cone_path_properties line 225
  12. def OAI.PackingSufficiencySupport.Hamiltonian.homogeneousConeField line 260
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.homogeneousCone_timePrimitive line 264
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_homogeneousCone_shell_flow line 280
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.moser_vector_natural line 319
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.linear_equivariant_fderiv line 331
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.hopfPrimitive_linear_invariant line 342
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.mixedHopfPrimitive_linear_invariant line 348
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.homogeneousConePrimitive_linear_invariant line 361
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.exterior_linear_invariant line 373
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.homogeneousConeField_linear_invariant line 385
  22. def OAI.PackingSufficiencySupport.Hamiltonian.phaseRotate line 416
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseRotate_apply line 420
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseRotate_smooth line 423
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseRotate_zero line 429
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseRotate_add line 433
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseRotate_period line 439
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseRotate_hasDerivAt line 443
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseCircle_smooth line 451
  30. def OAI.PackingSufficiencySupport.Hamiltonian.phaseCircleAction line 466
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseCircleAction_generator line 473
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseSq_rotate line 485