OAI/Geometry/BallPacking/Toric/RadialDiskSmooth.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.diskForward_contDiffAt line 14
  2. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.diskForward_contDiff line 27
  3. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.diskRadius_contDiffAt line 36
  4. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.diskInverse_contDiffAt line 54
  5. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.diskInverse_contDiffOn line 68
  6. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.diskInverse_isEmbedding line 75
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexArea_scaled_derivative line 98
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexArea_fderiv_real_smul line 104
  9. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.inverseDiskScale_contDiffAt line 119
  10. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.diskInverse_angular_fst line 133
  11. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.diskInverse_angular_snd line 165
  12. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.diskInverse_angular_comp line 199
  13. def OAI.PackingSufficiencySupport.Hamiltonian.coefficientSquares line 229
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.coefficientSquares_contDiff line 231
  15. def OAI.PackingSufficiencySupport.Hamiltonian.normalizedToricLift line 236
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.coefficient_diskInverse_contDiffAt line 239
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.normalizedToricLift_contDiffAt line 249
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.normalizedToricLift_pullback_primitive line 264
  19. def OAI.PackingSufficiencySupport.CubicModel.physicalDiskCoordinates line 295
  20. theorem OAI.PackingSufficiencySupport.CubicModel.physicalDiskCoordinates_apply line 300
  21. theorem OAI.PackingSufficiencySupport.CubicModel.physicalDiskCoordinates_squared line 304
  22. theorem OAI.PackingSufficiencySupport.CubicModel.physicalDiskCoordinates_mem line 312
  23. theorem OAI.PackingSufficiencySupport.CubicModel.complexArea_real_smul_both line 318
  24. theorem OAI.PackingSufficiencySupport.CubicModel.physicalDiskCoordinates_area line 323
  25. theorem OAI.PackingSufficiencySupport.CubicModel.physicalDiskCoordinates_primitive line 335
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.normalizedToricLift_manifold_primitive line 352
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.affineFSPrimitive_hopf_manifold line 388
  28. def OAI.PackingSufficiencySupport.CubicModel.weightedCoefficient line 410
  29. theorem OAI.PackingSufficiencySupport.CubicModel.weightedCoefficient_smooth line 413
  30. theorem OAI.PackingSufficiencySupport.CubicModel.weightedCoefficient_nonzero line 419
  31. theorem OAI.PackingSufficiencySupport.CubicModel.weightedCoefficient_norm line 425
  32. theorem OAI.PackingSufficiencySupport.CubicModel.weightedCoefficient_hopf line 430
  33. def OAI.PackingSufficiencySupport.CubicModel.cubicCoefficients line 446
  34. theorem OAI.PackingSufficiencySupport.CubicModel.cubicCoefficients_smooth line 450
  35. theorem OAI.PackingSufficiencySupport.CubicModel.cubicCoefficients_squares line 455
  36. def OAI.PackingSufficiencySupport.CubicModel.physicalPolynomialLift line 461
  37. theorem OAI.PackingSufficiencySupport.CubicModel.physicalPolynomialLift_smoothAt line 465
  38. theorem OAI.PackingSufficiencySupport.CubicModel.physicalPolynomialLift_primitive line 477