OAI/Geometry/BallPacking/BallMaps/SphereCartesianDescent.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexConjugate_leftInverse line 16
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexConjugate_radius line 22
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexConjugate_circle line 27
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.sphereCartesianDescend_equiv line 41
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_degree_global_affine_moser line 70
  6. def OAI.PackingSufficiencySupport.DiagonalQuadrics.affineComplexEquiv line 132
  7. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.affineComplexEquiv_apply line 135
  8. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.affineComplexEquiv_symm_apply line 140
  9. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.affineComplex_cartesian line 143
  10. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.affineComplexEquiv_toCLM line 148
  11. def OAI.PackingSufficiencySupport.Hamiltonian.optionComplexAmbient line 162
  12. def OAI.PackingSufficiencySupport.Hamiltonian.optionPhaseAmbient line 171
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.optionPhaseAmbient_capacity line 174
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.optionPhaseAmbient_form line 183
  15. def OAI.PackingSufficiencySupport.Hamiltonian.fsBallHomeomorph line 194
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.fsBallMap_isEmbedding line 204
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexCartesian_standardForm line 210
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexRadialTarget_mem line 215
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_degree_polynomial_target_embedding line 221
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.affineFSForm_mul line 251
  21. def OAI.PackingSufficiencySupport.Hamiltonian.complexFSAffine line 256
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexFSAffine_smoothOn line 259
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexCartesian_ball_into line 269
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexCartesian_ball_isEmbedding line 275
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexCartesian_ball_codRestrict line 280
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexFSAffine_isEmbedding line 285
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexFSAffine_pullback line 291
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexFSAffine_ball_embedding line 309
  29. theorem OAI.PackingSufficiencySupport.CubicModel.exists_uniform_cubic_bubble_ball line 329
  30. def OAI.PackingSufficiencySupport.Hamiltonian.complexLeftBlock line 367
  31. def OAI.PackingSufficiencySupport.Hamiltonian.complexLeftBlockCLM line 370
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexLeftBlockCLM_apply line 377
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexLeftBlock_sq line 382
  34. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexLeftBlock_pairing line 387
  35. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexLeftBlock_hopf line 392
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexLeftBlock_primitive line 399
  37. def OAI.PackingSufficiencySupport.CubicModel.firstBubbleLift line 422
  38. theorem OAI.PackingSufficiencySupport.CubicModel.firstBubbleLift_smooth line 426
  39. theorem OAI.PackingSufficiencySupport.CubicModel.firstBubbleLift_coordinates line 435
  40. theorem OAI.PackingSufficiencySupport.CubicModel.firstBubbleLift_nonzero line 440
  41. theorem OAI.PackingSufficiencySupport.CubicModel.cubicOuterBubble_nonzero line 444
  42. def OAI.PackingSufficiencySupport.CubicModel.cubicOuterBubblePrimitive line 457
  43. theorem OAI.PackingSufficiencySupport.CubicModel.cubicOuterBubble_joint_real_smooth line 463
  44. theorem OAI.PackingSufficiencySupport.CubicModel.cubicOuterBubblePrimitive_joint_smooth line 490
  45. theorem OAI.PackingSufficiencySupport.CubicModel.cubicOuterBubblePrimitive_smooth_family line 506
  46. theorem OAI.PackingSufficiencySupport.CubicModel.cubicOuterBubblePrimitive_zero line 513