OAI/Geometry/BallPacking/SurfaceArea/SurfaceInteriorBoxes.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.Hamiltonian.SurfaceCoordinateBox.Inside line 19
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.SurfaceCoordinateBox.interior_overlap_chain line 21
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.SurfaceCoordinateBox.finite_partition_inside line 40
  4. def OAI.PackingSufficiencySupport.Hamiltonian.HasInteriorPrimitiveFamily line 69
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.HasInteriorPrimitiveFamily.add line 74
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.surface_box_difference_inside line 84
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.surface_overlap_difference_inside line 116
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.surface_bump_difference_inside line 141
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_interior_mass_transfer_data line 164
  10. def OAI.PackingSufficiencySupport.Hamiltonian.restrictSurfacePartition line 184
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.restrictSurfacePartition_subordinate line 192
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.partitionFormMass_restrict line 197
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.interior_surface_primitive line 209
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.exists_normalized_surface_primitive line 248
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothTwoFormFamily.coefficient_smul line 316
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_interior_boundary_cutoff line 347
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_interior_coefficient_difference line 375
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.interior_difference_mass line 405
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.restricted_form_mass_nonneg line 441
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.partitionFormMass_smooth line 460
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.partitionFormMass_sub line 473