OAI/Geometry/BallPacking/Projective/CubicEndCoordinates.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PackingSufficiencySupport.CubicModel.AffineIndex line 13
  2. abbrev OAI.PackingSufficiencySupport.CubicModel.HomogeneousIndex line 14
  3. abbrev OAI.PackingSufficiencySupport.CubicModel.EndIndex line 15
  4. def OAI.PackingSufficiencySupport.CubicModel.zeroEnd line 17
  5. def OAI.PackingSufficiencySupport.CubicModel.endQuotient line 19
  6. def OAI.PackingSufficiencySupport.CubicModel.removableCoordinate line 23
  7. def OAI.PackingSufficiencySupport.CubicModel.endRemovable line 26
  8. def OAI.PackingSufficiencySupport.CubicModel.endHomogeneous line 30
  9. def OAI.PackingSufficiencySupport.CubicModel.endRegular line 35
  10. def OAI.PackingSufficiencySupport.CubicModel.endRegularRegion line 38
  11. theorem OAI.PackingSufficiencySupport.CubicModel.endRegularRegion_open line 41
  12. theorem OAI.PackingSufficiencySupport.CubicModel.zero_mem_endRegularRegion line 56
  13. theorem OAI.PackingSufficiencySupport.CubicModel.endHomogeneous_contDiffAt line 61
  14. theorem OAI.PackingSufficiencySupport.CubicModel.endQuotient_contDiffAt line 72
  15. theorem OAI.PackingSufficiencySupport.CubicModel.endRemovable_contDiffAt line 82
  16. theorem OAI.PackingSufficiencySupport.CubicModel.endRegular_contDiffAt line 93
  17. theorem OAI.PackingSufficiencySupport.CubicModel.endHomogeneous_ne_zero line 111
  18. theorem OAI.PackingSufficiencySupport.CubicModel.endRegular_ne_zero line 131
  19. theorem OAI.PackingSufficiencySupport.CubicModel.endRegular_cartesian_ne_zero line 139
  20. theorem OAI.PackingSufficiencySupport.CubicModel.removableCoordinate_eq line 145
  21. theorem OAI.PackingSufficiencySupport.CubicModel.endQuotient_zeroEnd line 152
  22. theorem OAI.PackingSufficiencySupport.CubicModel.endQuotient_homogeneous line 159
  23. theorem OAI.PackingSufficiencySupport.CubicModel.endQuotient_phase line 167
  24. theorem OAI.PackingSufficiencySupport.CubicModel.cubic_infinityPhase_germ line 185
  25. abbrev OAI.PackingSufficiencySupport.Hamiltonian.VeroneseIndex line 203
  26. def OAI.PackingSufficiencySupport.Hamiltonian.veronese line 205
  27. def OAI.PackingSufficiencySupport.Hamiltonian.veroneseDerivative line 209
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.veronese_contDiff line 214
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.veronese_hasFDerivAt line 220
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.veronese_pairing line 228
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.veronese_sq line 241
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.veronese_phaseArea line 248
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.holomorphicCartesian_derivative_I line 257
  34. theorem OAI.PackingSufficiencySupport.Hamiltonian.holomorphicFS_nonnegative line 270
  35. theorem OAI.PackingSufficiencySupport.Hamiltonian.holomorphicFS_exterior line 281
  36. def OAI.PackingSufficiencySupport.DiagonalQuadrics.affineComplex line 301
  37. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.complexCartesian_affineComplex line 306
  38. abbrev OAI.PackingSufficiencySupport.DiagonalQuadrics.NormalPolynomialIndex line 310
  39. def OAI.PackingSufficiencySupport.DiagonalQuadrics.normalPolynomial line 312
  40. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.normalPolynomial_smooth line 316
  41. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.normalPolynomialCartesian_smooth line 324
  42. def OAI.PackingSufficiencySupport.DiagonalQuadrics.ambientFSPrimitive line 329
  43. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.ambientFSPrimitive_smooth line 332
  44. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.ambientFSPrimitive_exterior line 336
  45. def OAI.PackingSufficiencySupport.DiagonalQuadrics.normalAmbientPrimitive line 345
  46. def OAI.PackingSufficiencySupport.DiagonalQuadrics.normalAmbientForm line 349
  47. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.normalAmbientPrimitive_smooth line 352
  48. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.normalAmbientForm_apply line 358
  49. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.normalAmbientForm_positive line 373
  50. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.normalAmbientForm_isInvertible line 383
  51. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.normalAmbientForm_smooth line 388
  52. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.normalAmbientForm_closed line 392
  53. abbrev OAI.PackingSufficiencySupport.CubicModel.WeightedAffineIndex line 405
  54. abbrev OAI.PackingSufficiencySupport.CubicModel.WeightedHomogeneousIndex line 406
  55. def OAI.PackingSufficiencySupport.CubicModel.five line 408
  56. def OAI.PackingSufficiencySupport.CubicModel.weightedEndQuotient line 413
  57. def OAI.PackingSufficiencySupport.CubicModel.endCoefficient line 417
  58. def OAI.PackingSufficiencySupport.CubicModel.endNumerator line 420
  59. def OAI.PackingSufficiencySupport.CubicModel.weightedEndOrder line 423
  60. def OAI.PackingSufficiencySupport.CubicModel.weightedEndRegular line 426
  61. theorem OAI.PackingSufficiencySupport.CubicModel.five_contDiffAt line 438
  62. theorem OAI.PackingSufficiencySupport.CubicModel.endCoefficient_contDiffAt line 455
  63. theorem OAI.PackingSufficiencySupport.CubicModel.endNumerator_contDiffAt line 460
  64. theorem OAI.PackingSufficiencySupport.CubicModel.complexAffineLift_holomorphic line 464
  65. theorem OAI.PackingSufficiencySupport.CubicModel.weightedEndRegular_contDiffAt line 472
  66. theorem OAI.PackingSufficiencySupport.CubicModel.endCoordinate_false line 495
  67. theorem OAI.PackingSufficiencySupport.CubicModel.weightedEndQuotient_contDiffAt line 505
  68. theorem OAI.PackingSufficiencySupport.CubicModel.weightedEndRegular_none line 511
  69. theorem OAI.PackingSufficiencySupport.CubicModel.weightedEndRegular_ne_zero line 516
  70. theorem OAI.PackingSufficiencySupport.CubicModel.weightedEndRegular_cartesian_ne_zero line 531
  71. theorem OAI.PackingSufficiencySupport.CubicModel.scale_div_pow line 536
  72. theorem OAI.PackingSufficiencySupport.CubicModel.scale_complement_pow line 540
  73. theorem OAI.PackingSufficiencySupport.CubicModel.scale_div_mixed line 548
  74. theorem OAI.PackingSufficiencySupport.CubicModel.scale_regular_pow line 554
  75. theorem OAI.PackingSufficiencySupport.CubicModel.scale_onepole_mixed line 559
  76. theorem OAI.PackingSufficiencySupport.CubicModel.scale_onepole_cross line 565
  77. def OAI.PackingSufficiencySupport.CubicModel.weightedLift line 571
  78. theorem OAI.PackingSufficiencySupport.CubicModel.weightedLift_scale_poles line 574
  79. theorem OAI.PackingSufficiencySupport.CubicModel.weightedLift_scale_left line 591
  80. theorem OAI.PackingSufficiencySupport.CubicModel.weightedLift_scale_right line 607
  81. theorem OAI.PackingSufficiencySupport.CubicModel.weightedEndRegular_scale line 631
  82. theorem OAI.PackingSufficiencySupport.CubicModel.weightedEndQuotient_phase line 651
  83. theorem OAI.PackingSufficiencySupport.CubicModel.weighted_infinityPhase_germ line 664
  84. theorem OAI.PackingSufficiencySupport.Hamiltonian.logarithmicDerivative_pow line 684
  85. theorem OAI.PackingSufficiencySupport.Hamiltonian.hopfPrimitive_variable_power_gauge line 694
  86. theorem OAI.PackingSufficiencySupport.Hamiltonian.planar_power_gauge line 713
  87. def OAI.PackingSufficiencySupport.CubicModel.weightedRegularEndPhase line 742
  88. def OAI.PackingSufficiencySupport.CubicModel.weightedRegularEndPrimitive line 745
  89. def OAI.PackingSufficiencySupport.CubicModel.weightedEndResidue line 748
  90. theorem OAI.PackingSufficiencySupport.CubicModel.weightedRegularEndPhase_contDiffAt line 750
  91. theorem OAI.PackingSufficiencySupport.CubicModel.weightedRegularEndPrimitive_contDiffAt line 757
  92. theorem OAI.PackingSufficiencySupport.CubicModel.weightedEndQuotientPrimitive_residue line 764
  93. theorem OAI.PackingSufficiencySupport.CubicModel.weightedFSPrimitive_infinity line 797
  94. theorem OAI.PackingSufficiencySupport.CubicModel.sum_weightedEndResidue line 819