OAI/Geometry/BallPacking/Hopf/DegreeRelativeShell.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_shell_profile line 15
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.cutoffDegreeForm_shell line 28
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_degree_relative_shell_maps line 39
  4. def OAI.PackingSufficiencySupport.Hamiltonian.phaseOptionSplit line 117
  5. def OAI.PackingSufficiencySupport.Hamiltonian.phaseInfinityInclusion line 126
  6. def OAI.PackingSufficiencySupport.Hamiltonian.phaseInfinityProjection line 127
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseInfinityInclusion_none line 130
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseInfinityInclusion_some line 131
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseInfinity_left line 132
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseInfinity_embedding line 133
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseInfinity_dot line 136
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseInfinity_area line 140
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseInfinity_J line 144
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseInfinity_range line 147
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseInfinity_complex_range line 156
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseUnitDiagonal_eq_rotate line 167
  17. def OAI.PackingSufficiencySupport.Hamiltonian.complexQuotientGauge line 188
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexQuotientGauge_smoothAt line 191
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexQuotientGauge_ne line 198
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexSphereLift_quotient_gauge line 202
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.mixedHopfCurvaturePullback_sphereLift line 209
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.mixedHopfCurvaturePullback_chart_normalize line 228
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.degreeHopfCurvaturePullback_sphereLift line 247
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.degreeHopfCurvaturePullback_chart_normalize line 266
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.sphere_map_fderiv_tangent line 283
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.homogeneousCone_sphere_tangent line 294
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.cone_flow_sphere_pullback line 302
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.degreeCone_sphere_tangent line 330
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.degree_cone_flow_sphere_pullback line 338
  30. def OAI.PackingSufficiencySupport.Hamiltonian.sphereAffineDescend line 371
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.sphereAffineDescend_smooth line 374
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.sphereAffineDescend_leftInverse line 385
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.sphereAffineDescend_equiv line 404
  34. def OAI.PackingSufficiencySupport.Hamiltonian.complexConjugate line 425
  35. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexConjugate_smooth line 428
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.sphereAffineDescend_curvature line 432
  37. theorem OAI.PackingSufficiencySupport.Hamiltonian.sphereAffineDescend_degree_curvature line 495