OAI/Geometry/BallPacking/DiskMaps/NormalizedRoundedBoxes.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.Hamiltonian.normalizedRoundedMap line 13
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.normalizedRoundedMap_smooth line 16
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.normalizedRoundedMap_injective line 20
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.normalizedRoundedMap_det_pos line 26
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.normalizedRoundedMap_image line 37
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.roundedBox_volume_eq line 42
  7. def OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopyFamily.cutoff line 62
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopyFamily.endpoint_support line 75
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopyFamily.cutoff_compact line 83
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopyFamily.exists_compact_parameterization line 96
  11. def OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopyFamily.timeCutoff line 113
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopyFamily.joint_support line 126
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopyFamily.timeCutoff_hasCompactSupport line 135
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopyFamily.exists_joint_compact line 149
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_parameter_relative_circle_primitive line 172
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.parameter_relative_finite_potential_correction line 253
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_parameter_relative_finite_circle_correction line 301
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_parameter_relative_density_transport line 331
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_parameter_relative_primitive line 383
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_parameter_relative_background_moser line 451