OAI/Geometry/BallPacking/Hopf/DegreeHopfDeformation.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.Hamiltonian.degreeHopfPrimitive line 14
  2. def OAI.PackingSufficiencySupport.Hamiltonian.degreeHopfForm line 18
  3. def OAI.PackingSufficiencySupport.Hamiltonian.degreeConePrimitive line 21
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.degreeHopfPrimitive_smoothAt line 25
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.degreeHopfForm_eq line 31
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.degreeHopfPrimitive_circle line 42
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.degreeHopfForm_radial line 51
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.degreeHopfForm_circle line 59
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.degreeHopfForm_skew line 67
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.degreeHopfForm_horizontal_positive line 72
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.degreeConePrimitive_exterior line 88
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.degreeConePrimitive_nondegenerate line 101
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.degreeConePrimitive_circle_contraction line 119
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.degreeConePrimitive_smoothAt line 128
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.degreeConePrimitive_affine line 133
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.degreeConePrimitive_circle line 142
  17. def OAI.PackingSufficiencySupport.Hamiltonian.degreeHopfCurvaturePullback line 152
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.degreeHopfCurvaturePullback_gauge line 157
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.degreeHopfCurvaturePullback_eq line 181
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.hopfCurvaturePullback_comp line 207
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.mixedHopfCurvaturePullback_comp line 218
  22. def OAI.PackingSufficiencySupport.Hamiltonian.degreeAffineForm line 237
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.degreeAffineForm_apply line 246
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.degreeHopfCurvaturePullback_comp line 250
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.degreeAffineForm_pullback line 263
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.degreeAffineForm_zero line 271
  27. def OAI.PackingSufficiencySupport.CubicModel.cubicBubblePrimitive line 286
  28. theorem OAI.PackingSufficiencySupport.CubicModel.distinguishedResidualTerm_real_smooth line 293
  29. theorem OAI.PackingSufficiencySupport.CubicModel.distinguishedResidualPolynomial_real_smooth line 303
  30. theorem OAI.PackingSufficiencySupport.CubicModel.cubicBubbleResidual_real_smooth line 310
  31. theorem OAI.PackingSufficiencySupport.CubicModel.cubicBubblePrimitive_joint_smooth line 327
  32. theorem OAI.PackingSufficiencySupport.CubicModel.cubicBubblePrimitive_smooth_family line 342
  33. theorem OAI.PackingSufficiencySupport.CubicModel.cubicBubblePrimitive_zero line 348
  34. theorem OAI.PackingSufficiencySupport.CubicModel.cubicBubblePrimitive_zero_exterior line 369
  35. theorem OAI.PackingSufficiencySupport.CubicModel.cubicBubblePrimitive_zero_invertible line 381
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.residualPrimitive_exterior line 403
  37. theorem OAI.PackingSufficiencySupport.Hamiltonian.residual_degreeAffineForm line 427
  38. theorem OAI.PackingSufficiencySupport.CubicModel.cubicBubblePolynomial_real_smooth line 454
  39. theorem OAI.PackingSufficiencySupport.CubicModel.cubicBubbleResidual_fixed_real_smooth line 459
  40. theorem OAI.PackingSufficiencySupport.CubicModel.cubicBubblePrimitive_curvature line 464
  41. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_uniform_compact_exact_fibre_embedding_into line 503