OAI/Geometry/BallPacking/BallMaps/SixCubicInnerNormalPacking.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.CubicModel.actual_six_cubic_inner_normal_packing line 14
  2. theorem OAI.PackingSufficiencySupport.CubicModel.actual_six_cubic_inner_polynomial_packing_avoid_axes line 81
  3. theorem OAI.PackingSufficiencySupport.CubicModel.actual_six_cubic_inner_polynomial_packing line 124
  4. theorem OAI.PackingSufficiencySupport.CubicModel.actual_six_quadric_polynomial_packing line 138
  5. def OAI.PackingSufficiencySupport.CubicModel.cubicOuterBubbleForm line 197
  6. theorem OAI.PackingSufficiencySupport.CubicModel.exists_uniform_outer_bubble_transfer line 200
  7. theorem OAI.PackingSufficiencySupport.CubicModel.outer_packing_uniform_bubble line 242
  8. theorem OAI.PackingSufficiencySupport.CubicModel.outer_packing_uniform_bubble_into line 288
  9. def OAI.PackingSufficiencySupport.CubicModel.firstToDistinguished line 335
  10. def OAI.PackingSufficiencySupport.CubicModel.distinguishedToFirst line 338
  11. theorem OAI.PackingSufficiencySupport.CubicModel.firstToDistinguished_smoothAt line 341
  12. theorem OAI.PackingSufficiencySupport.CubicModel.distinguishedToFirst_smoothAt line 352
  13. theorem OAI.PackingSufficiencySupport.CubicModel.distinguishedToFirst_first line 360
  14. theorem OAI.PackingSufficiencySupport.CubicModel.firstToDistinguished_first line 366
  15. def OAI.PackingSufficiencySupport.CubicModel.firstDistinguishedHomeomorph line 371
  16. theorem OAI.PackingSufficiencySupport.CubicModel.firstToDistinguished_isEmbedding line 388
  17. theorem OAI.PackingSufficiencySupport.CubicModel.firstToDistinguished_lift line 392
  18. theorem OAI.PackingSufficiencySupport.CubicModel.firstToDistinguished_lift_near line 400
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.hopfCurvaturePullback_congr_near line 415
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.degreeHopfCurvaturePullback_congr_near line 423
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.homogeneousMixedPrimitive_exterior line 431
  22. theorem OAI.PackingSufficiencySupport.CubicModel.cubicOuterBubbleForm_homogeneous line 456
  23. theorem OAI.PackingSufficiencySupport.CubicModel.firstToDistinguished_curvature line 468