OAI/Geometry/BallPacking/Hamiltonian/AnnularDensityMass.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.densityChart_coefficient line 19
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.density_nonnegative line 30
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.rectangle_integral line 62
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.density_mass line 78
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.exists_surface_step_two line 126
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.exists_surface_normal_form_packing line 208
  7. def OAI.PackingSufficiencySupport.Hamiltonian.toricPrimitiveInterpolation line 283
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricPrimitiveInterpolation_zero line 287
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricPrimitiveInterpolation_one line 291
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricPrimitiveInterpolation_smooth line 294
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricPrimitiveInterpolation_exterior line 300
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricPrimitiveInterpolation_isInvertible line 324
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.toric_redistribution_moser line 353
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.exists_surface_initial_packing line 410
  15. structure OAI.PackingSufficiencySupport.Hamiltonian.PlanarHamiltonianMotion line 488
  16. def OAI.PackingSufficiencySupport.Hamiltonian.HamiltonianDiskIsotopyFamily.motion line 500