OAI/Geometry/BallPacking/Moments/RadialSlopes.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.FiniteMoment.Radial.slopeNumerator line 14
  2. def OAI.PackingSufficiencySupport.FiniteMoment.Radial.slope line 18
  3. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.slopeNumerator_contDiff line 21
  4. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.slope_contDiffAt line 25
  5. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.slopeNumerator_fst_pos line 30
  6. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.slopeNumerator_snd_pos line 41
  7. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.slope_pos line 52
  8. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.moment_eq_radius_slope line 59
  9. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.moment_eq_of_centered line 91
  10. abbrev OAI.PackingSufficiencySupport.FiniteMoment.MomentPlane line 102
  11. def OAI.PackingSufficiencySupport.FiniteMoment.planeVector line 103
  12. def OAI.PackingSufficiencySupport.FiniteMoment.trapezoidCorners line 104
  13. def OAI.PackingSufficiencySupport.FiniteMoment.openTrapezoid line 106
  14. theorem OAI.PackingSufficiencySupport.FiniteMoment.openTrapezoid_isOpen line 109
  15. theorem OAI.PackingSufficiencySupport.FiniteMoment.trapezoid_mem_convexHull line 116
  16. theorem OAI.PackingSufficiencySupport.FiniteMoment.trapezoid_interior line 140
  17. def OAI.PackingSufficiencySupport.FiniteMoment.TrapezoidWeight line 148
  18. def OAI.PackingSufficiencySupport.FiniteMoment.trapezoidWeight line 152
  19. instance OAI.PackingSufficiencySupport.FiniteMoment.trapezoidWeight_nonempty line 155
  20. theorem OAI.PackingSufficiencySupport.FiniteMoment.trapezoidWeight_corners line 158
  21. theorem OAI.PackingSufficiencySupport.FiniteMoment.trapezoidWeight_surrounds line 171
  22. theorem OAI.PackingSufficiencySupport.FiniteMoment.trapezoidWeight_unique_moment line 175
  23. def OAI.PackingSufficiencySupport.FiniteMoment.Radial.weight line 188
  24. def OAI.PackingSufficiencySupport.FiniteMoment.Radial.logRadius line 190
  25. def OAI.PackingSufficiencySupport.FiniteMoment.Radial.expRadius line 192
  26. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.expRadius_logRadius line 194
  27. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.monomial_expRadius line 198
  28. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.polynomial_expRadius line 203
  29. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.moment_expRadius line 210
  30. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.exists_positive_radial_solution line 219
  31. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.positive_radial_unique line 229
  32. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.moment_axis_fst line 242
  33. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.moment_origin line 252
  34. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.active_origin_pos line 264
  35. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.centeredDerivative_axis_isInvertible line 286
  36. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.exists_smooth_axis_radial_solution line 325
  37. theorem OAI.PackingSufficiencySupport.FiniteMoment.exp_difference_strict line 359
  38. theorem OAI.PackingSufficiencySupport.FiniteMoment.gradient_zero_unique_of_separates line 366
  39. theorem OAI.PackingSufficiencySupport.FiniteMoment.moment_unique_of_separates line 390
  40. abbrev OAI.PackingSufficiencySupport.FiniteMoment.Radial.Face line 406
  41. def OAI.PackingSufficiencySupport.FiniteMoment.Radial.faceWeight line 408
  42. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.sum_face line 410
  43. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.polynomial_face_exp line 416
  44. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.numerator_face_exp_snd line 430
  45. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.moment_face_exp line 445
  46. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.interval_surrounds line 455
  47. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.interval_separates line 472
  48. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.exists_axis_solution line 483
  49. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.positive_axis_unique line 495