OAI/Geometry/BallPacking/Hopf/AffineHopfRestriction.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.Hamiltonian.complexAffineTangent line 13
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexAffineTangent_none line 19
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexAffineTangent_some line 21
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexAffineLift_hasFDerivAt line 23
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexAffineLift_fderiv line 36
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexPairing_affine_tangent line 39
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexPairing_tangent_tangent line 43
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.hopfForm_affine_restriction line 47
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.hopfForm_affine_pullback line 71
  10. def OAI.PackingSufficiencySupport.Hamiltonian.bubbleCoordinates line 91
  11. def OAI.PackingSufficiencySupport.Hamiltonian.homogeneousBubble line 95
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.bubbleCoordinates_smooth line 98
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.homogeneousBubble_joint_smooth line 105
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.bubbleCoordinates_smul line 113
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.homogeneousBubble_homogeneous line 119
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.bubbleCoordinates_affine line 129
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.homogeneousBubble_scaled line 135
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.homogeneousBubble_zero line 143
  19. def OAI.PackingSufficiencySupport.Hamiltonian.bubblePolynomial line 149
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.bubblePolynomial_joint_smooth line 153
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.bubblePolynomial_homogeneous line 163
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.bubblePolynomial_nonzero line 175
  23. def OAI.PackingSufficiencySupport.CubicModel.distinguishedChart line 191
  24. def OAI.PackingSufficiencySupport.CubicModel.distinguishedResidualTerm line 194
  25. theorem OAI.PackingSufficiencySupport.CubicModel.distinguishedResidualTerm_smooth line 198
  26. theorem OAI.PackingSufficiencySupport.CubicModel.distinguishedResidualTerm_factor line 203
  27. def OAI.PackingSufficiencySupport.CubicModel.distinguishedResidualPolynomial line 223
  28. theorem OAI.PackingSufficiencySupport.CubicModel.distinguishedResidualPolynomial_smooth line 230
  29. theorem OAI.PackingSufficiencySupport.CubicModel.outerPolynomial_distinguished_factor line 236
  30. theorem OAI.PackingSufficiencySupport.CubicModel.distinguishedResidualPolynomial_zero line 256
  31. def OAI.PackingSufficiencySupport.CubicModel.distinguishedHomogeneousCoordinates line 270
  32. theorem OAI.PackingSufficiencySupport.CubicModel.distinguishedHomogeneousCoordinates_smooth line 273
  33. theorem OAI.PackingSufficiencySupport.CubicModel.distinguishedHomogeneousCoordinates_smul line 279
  34. theorem OAI.PackingSufficiencySupport.CubicModel.distinguishedHomogeneousCoordinates_chart line 284
  35. theorem OAI.PackingSufficiencySupport.CubicModel.complexAffineLift_complex_smooth line 289
  36. def OAI.PackingSufficiencySupport.CubicModel.cubicBubblePolynomial line 296
  37. def OAI.PackingSufficiencySupport.CubicModel.cubicBubbleResidual line 300
  38. theorem OAI.PackingSufficiencySupport.CubicModel.cubicBubblePolynomial_joint_smooth line 308
  39. theorem OAI.PackingSufficiencySupport.CubicModel.cubicBubbleResidual_joint_smooth line 314
  40. theorem OAI.PackingSufficiencySupport.CubicModel.cubicBubblePolynomial_homogeneous line 326
  41. theorem OAI.PackingSufficiencySupport.CubicModel.cubicBubblePolynomial_nonzero line 339
  42. theorem OAI.PackingSufficiencySupport.CubicModel.cubicBubblePolynomial_scaled line 344
  43. theorem OAI.PackingSufficiencySupport.CubicModel.cubicBubbleResidual_nonzero line 356
  44. theorem OAI.PackingSufficiencySupport.CubicModel.cubicBubbleResidual_zero line 364
  45. theorem OAI.PackingSufficiencySupport.Hamiltonian.phasePowerMap_dot line 386
  46. theorem OAI.PackingSufficiencySupport.Hamiltonian.phasePowerMap_area line 398
  47. theorem OAI.PackingSufficiencySupport.Hamiltonian.homogeneousVeronese_hopf line 406
  48. def OAI.PackingSufficiencySupport.Hamiltonian.complexMiddleBlock line 440
  49. def OAI.PackingSufficiencySupport.Hamiltonian.complexMiddleBlockCLM line 443
  50. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexMiddleBlockCLM_apply line 450
  51. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexMiddleBlock_sq line 455
  52. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexMiddleBlock_pairing line 460
  53. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexMiddleBlock_hopf line 465
  54. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexMiddleBlock_primitive line 472
  55. theorem OAI.PackingSufficiencySupport.Hamiltonian.homogeneousVeronese_affinePrimitive line 488
  56. theorem OAI.PackingSufficiencySupport.Hamiltonian.fibrePrimitivePullback_smooth line 514