OAI/Geometry/BallPacking/Moments/ExponentialMoment.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.FiniteMoment.partition line 16
  2. def OAI.PackingSufficiencySupport.FiniteMoment.gradient line 18
  3. def OAI.PackingSufficiencySupport.FiniteMoment.moment line 20
  4. def OAI.PackingSufficiencySupport.FiniteMoment.Surrounds line 22
  5. theorem OAI.PackingSufficiencySupport.FiniteMoment.partition_pos line 25
  6. theorem OAI.PackingSufficiencySupport.FiniteMoment.partition_contDiff line 33
  7. theorem OAI.PackingSufficiencySupport.FiniteMoment.partition_hasFDerivAt line 39
  8. theorem OAI.PackingSufficiencySupport.FiniteMoment.partition_coercive line 48
  9. theorem OAI.PackingSufficiencySupport.FiniteMoment.exists_gradient_zero line 66
  10. theorem OAI.PackingSufficiencySupport.FiniteMoment.exp_difference_nonneg line 79
  11. theorem OAI.PackingSufficiencySupport.FiniteMoment.exp_difference_pos line 86
  12. theorem OAI.PackingSufficiencySupport.FiniteMoment.gradient_zero_unique line 91
  13. theorem OAI.PackingSufficiencySupport.FiniteMoment.gradient_center line 119
  14. theorem OAI.PackingSufficiencySupport.FiniteMoment.moment_eq_iff_gradient_center_zero line 130
  15. theorem OAI.PackingSufficiencySupport.FiniteMoment.exists_unique_moment line 138
  16. theorem OAI.PackingSufficiencySupport.FiniteMoment.surrounds_of_interior line 147
  17. theorem OAI.PackingSufficiencySupport.FiniteMoment.surrounds_isOpen line 177
  18. theorem OAI.PackingSufficiencySupport.FiniteMoment.exists_unique_moment_interior line 193
  19. def OAI.PackingSufficiencySupport.FiniteMoment.hessian line 203
  20. theorem OAI.PackingSufficiencySupport.FiniteMoment.hessian_apply line 206
  21. theorem OAI.PackingSufficiencySupport.FiniteMoment.gradient_hasFDerivAt line 210
  22. theorem OAI.PackingSufficiencySupport.FiniteMoment.hessian_inner line 219
  23. theorem OAI.PackingSufficiencySupport.FiniteMoment.hessian_positive line 228
  24. theorem OAI.PackingSufficiencySupport.FiniteMoment.hessian_isInvertible line 239
  25. theorem OAI.PackingSufficiencySupport.FiniteMoment.surrounds_separates line 254
  26. theorem OAI.PackingSufficiencySupport.FiniteMoment.centeredGradient_contDiff line 260
  27. def OAI.PackingSufficiencySupport.FiniteMoment.inverse line 273
  28. theorem OAI.PackingSufficiencySupport.FiniteMoment.inverse_spec line 275
  29. theorem OAI.PackingSufficiencySupport.FiniteMoment.inverse_unique line 279
  30. theorem OAI.PackingSufficiencySupport.FiniteMoment.positiveCoefficients_isOpen line 284
  31. theorem OAI.PackingSufficiencySupport.FiniteMoment.inverse_contDiffAt line 291
  32. theorem OAI.PackingSufficiencySupport.FiniteMoment.inverse_contDiffOn line 322
  33. abbrev OAI.PackingSufficiencySupport.FiniteMoment.Radial.Plane line 333
  34. def OAI.PackingSufficiencySupport.FiniteMoment.Radial.monomial line 336
  35. def OAI.PackingSufficiencySupport.FiniteMoment.Radial.polynomial line 338
  36. def OAI.PackingSufficiencySupport.FiniteMoment.Radial.numerator line 341
  37. def OAI.PackingSufficiencySupport.FiniteMoment.Radial.moment line 345
  38. def OAI.PackingSufficiencySupport.FiniteMoment.Radial.centered line 348
  39. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.monomial_nonneg line 352
  40. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.polynomial_pos line 355
  41. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.polynomial_contDiff line 366
  42. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.centered_contDiff line 373
  43. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.centered_eq line 377
  44. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.centered_moment line 393
  45. def OAI.PackingSufficiencySupport.FiniteMoment.Radial.monomialDerivative line 397
  46. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.monomial_hasFDerivAt line 401
  47. def OAI.PackingSufficiencySupport.FiniteMoment.Radial.centeredDerivative line 411
  48. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.centered_hasFDerivAt line 415
  49. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.centeredDerivative_apply line 423
  50. def OAI.PackingSufficiencySupport.FiniteMoment.Radial.faceMass line 433
  51. def OAI.PackingSufficiencySupport.FiniteMoment.Radial.transverse line 435
  52. def OAI.PackingSufficiencySupport.FiniteMoment.Radial.active line 438
  53. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.zero_power_derivative line 441
  54. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.monomial_axis line 449
  55. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.monomialDerivative_axis line 455
  56. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.centered_axis_snd line 468
  57. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.centeredDerivative_axis_fst line 475
  58. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.centeredDerivative_axis_snd line 488
  59. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.transverse_pos line 497
  60. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.nat_mul_power line 508
  61. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.active_variance line 515
  62. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.active_pos line 534