OAI/Geometry/BallPacking/Moments/RearrangementBounds.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.MomentPolytope.successive_bound line 16
  2. theorem OAI.PackingSufficiencySupport.MomentPolytope.successive_increasing line 23
  3. def OAI.PackingSufficiencySupport.MomentPolytope.fullRearrangement line 38
  4. theorem OAI.PackingSufficiencySupport.MomentPolytope.fullRearrangement_increasing line 41
  5. theorem OAI.PackingSufficiencySupport.MomentPolytope.increasing_min_at_zero line 49
  6. theorem OAI.PackingSufficiencySupport.MomentPolytope.volume_region_pos line 74
  7. theorem OAI.PackingSufficiencySupport.MomentPolytope.volume_region_toReal_pos line 104
  8. def OAI.PackingSufficiencySupport.Comparison.averageMap line 118
  9. theorem OAI.PackingSufficiencySupport.Comparison.averageMap_mono line 121
  10. theorem OAI.PackingSufficiencySupport.Comparison.averageMap_const line 125
  11. theorem OAI.PackingSufficiencySupport.Comparison.averageMap_lower line 130
  12. theorem OAI.PackingSufficiencySupport.MomentPolytope.analytic_gap line 143
  13. theorem OAI.PackingSufficiencySupport.Comparison.smooth_approximation line 185
  14. theorem OAI.HigherDimensionalBallPacking.hasPacking_iff_support line 210
  15. theorem OAI.HigherDimensionalBallPacking.HasPacking.volume_lt line 225
  16. def OAI.PackingSufficiencySupport.Hamiltonian.outerMoments line 239
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.outerMoments_self line 243
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.outerMoments_other line 247
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.outerMoments_smooth line 250
  20. def OAI.PackingSufficiencySupport.Hamiltonian.outerDifferential line 259
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.outerMoments_hasFDerivAt line 263
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.outerMoments_fderiv_apply line 273
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.outerMoments_fderiv_single line 280
  24. def OAI.PackingSufficiencySupport.Hamiltonian.HamiltonianDiskIsotopyFamily.refl line 298
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.HamiltonianDiskIsotopyFamily.mapsTo_closed line 318
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialArea_nonneg line 330
  27. def OAI.PackingSufficiencySupport.MomentPolytope.baseProjection line 342
  28. def OAI.PackingSufficiencySupport.MomentPolytope.baseProjectionL line 344
  29. theorem OAI.PackingSufficiencySupport.MomentPolytope.baseProjection_smooth line 349
  30. theorem OAI.PackingSufficiencySupport.MomentPolytope.assemble_zero_smooth line 352
  31. theorem OAI.PackingSufficiencySupport.MomentPolytope.baseProjection_assemble line 361
  32. def OAI.PackingSufficiencySupport.MomentPolytope.fullBase line 364
  33. theorem OAI.PackingSufficiencySupport.MomentPolytope.fullBase_eq_image line 367
  34. theorem OAI.PackingSufficiencySupport.MomentPolytope.fullBase_compact line 380
  35. theorem OAI.PackingSufficiencySupport.MomentPolytope.fullBase_convex line 385
  36. def OAI.PackingSufficiencySupport.MomentPolytope.fullLength line 393
  37. theorem OAI.PackingSufficiencySupport.MomentPolytope.continuous_fullLength line 395
  38. theorem OAI.PackingSufficiencySupport.MomentPolytope.concave_fullLength line 398
  39. def OAI.PackingSufficiencySupport.MomentPolytope.activeParameters line 403
  40. theorem OAI.PackingSufficiencySupport.MomentPolytope.activeParameters_compact line 406
  41. theorem OAI.PackingSufficiencySupport.MomentPolytope.activeParameters_convex line 410
  42. def OAI.PackingSufficiencySupport.Hamiltonian.planeMoments line 421
  43. theorem OAI.PackingSufficiencySupport.Hamiltonian.planeMoments_smooth line 424
  44. theorem OAI.PackingSufficiencySupport.Hamiltonian.planeMoments_nonneg line 430
  45. def OAI.PackingSufficiencySupport.Hamiltonian.momentDifferential line 433
  46. theorem OAI.PackingSufficiencySupport.Hamiltonian.planeMoments_hasFDerivAt line 437
  47. theorem OAI.PackingSufficiencySupport.Hamiltonian.planeMoments_fderiv_apply line 445
  48. theorem OAI.PackingSufficiencySupport.Hamiltonian.planeMoments_fderiv_single line 450
  49. def OAI.PackingSufficiencySupport.Hamiltonian.toricHamiltonian line 458
  50. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricHamiltonian_smooth line 461
  51. def OAI.PackingSufficiencySupport.Hamiltonian.toricAngularSpeed line 464
  52. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricAngularSpeed_smooth line 467
  53. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricHamiltonian_fderiv_single line 471
  54. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricHamiltonian_field line 484
  55. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricHamiltonian_preserves_moments line 500