OAI/Geometry/BallPacking/Models/SurfaceComparison.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.MomentPolytope.compact_positive_lower line 13
  2. theorem OAI.PackingSufficiencySupport.MomentPolytope.inverse_comparison_gap line 20
  3. theorem OAI.PackingSufficiencySupport.MomentPolytope.finite_surface_comparison line 39
  4. theorem OAI.PackingSufficiencySupport.MomentPolytope.finite_uniform_area_error line 97
  5. def OAI.PackingSufficiencySupport.MomentPolytope.strictRegion line 105
  6. theorem OAI.PackingSufficiencySupport.MomentPolytope.strictRegion_subset line 108
  7. theorem OAI.PackingSufficiencySupport.MomentPolytope.strictRegion_phase_open line 111
  8. theorem OAI.PackingSufficiencySupport.MomentPolytope.planeRegion_outer_constraints line 120
  9. theorem OAI.PackingSufficiencySupport.MomentPolytope.momentFace_smooth line 126
  10. theorem OAI.PackingSufficiencySupport.MomentPolytope.face_collars_of_comparison line 129
  11. theorem OAI.PackingSufficiencySupport.MomentPolytope.comparison_preserves_region line 145
  12. theorem OAI.PackingSufficiencySupport.MomentPolytope.Annular.surface_packing_tolerance line 169
  13. theorem OAI.PackingSufficiencySupport.MomentPolytope.Annular.intrinsic_surface_packing_tolerance line 227
  14. theorem OAI.PackingSufficiencySupport.MomentPolytope.Annular.exhausted_surface_packing line 274
  15. def OAI.PackingSufficiencySupport.Hamiltonian.surfaceFormRatio line 336
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.surface_form_scalar_in_chart line 340
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.surface_form_scalar line 360
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceFormRatio_eq_chart line 368
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceFormRatio_smooth line 382
  20. theorem OAI.PackingSufficiencySupport.MomentPolytope.Annular.exhausted_curvature_surface_packing line 426