OAI/Geometry/BallPacking/Normal/CompactUniformCentral.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_uniform_compact_exact_fibre_embedding_central_into line 17
  2. theorem OAI.PackingSufficiencySupport.CubicModel.cubicBubblePrimitive_coefficient_affine line 66
  3. theorem OAI.PackingSufficiencySupport.CubicModel.cubicBubbleVariable_joint_smooth line 73
  4. theorem OAI.PackingSufficiencySupport.CubicModel.cubicBubbleVariable_smooth_family line 87
  5. theorem OAI.PackingSufficiencySupport.CubicModel.exists_uniform_cubic_bubble_transfer line 93
  6. def OAI.PackingSufficiencySupport.Hamiltonian.degreeHopfDifference line 150
  7. def OAI.PackingSufficiencySupport.Hamiltonian.radialDegreeConePrimitive line 153
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.degreeConePrimitive_split line 156
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.degreeHopfDifference_smoothAt line 165
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.degreeHopfDifference_circle line 171
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialDegreeConePrimitive_smoothAt line 180
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialDegreeConePrimitive_exterior line 192
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialDegreeConePrimitive_nondegenerate line 227
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialDegreeConePrimitive_circle_contraction line 248
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.radial_moser_field_tangent line 268
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseSq_nonautonomous_flow_constant line 284
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.exact_path_transport_on_unit_interval line 301
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_compact_radial_exact_moser line 341