OAI/Geometry/BallPacking/Hamiltonian/CartesianMomentSlices.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.scaled_disk_slice_iff line 14
  2. def OAI.PackingSufficiencySupport.MomentPolytope.planeRegion line 37
  3. theorem OAI.PackingSufficiencySupport.MomentPolytope.assemble_outerMoments line 40
  4. theorem OAI.PackingSufficiencySupport.MomentPolytope.baseProjection_outerMoments line 47
  5. theorem OAI.PackingSufficiencySupport.MomentPolytope.planeRegion_mem_iff line 52
  6. def OAI.PackingSufficiencySupport.MomentPolytope.globalSliceFamily line 63
  7. theorem OAI.PackingSufficiencySupport.MomentPolytope.globalSliceFamily_convex line 73
  8. theorem OAI.PackingSufficiencySupport.MomentPolytope.globalSliceFamily_at_moments line 90
  9. theorem OAI.PackingSufficiencySupport.MomentPolytope.coordRearrange_eq_intervalMinimum line 96
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_hamiltonian_rounded_intervals line 122
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_smooth_nested_intervals_of_room line 227
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_hamiltonian_unit_grid line 259
  13. theorem OAI.PackingSufficiencySupport.Comparison.exists_fine_unit_grid line 299
  14. theorem OAI.PackingSufficiencySupport.Comparison.exists_uniform_unit_modulus line 340
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_hamiltonian_unit_rearrangement line 366
  16. def OAI.PackingSufficiencySupport.Hamiltonian.liftArgument line 406
  17. def OAI.PackingSufficiencySupport.Hamiltonian.liftedHamiltonian line 409
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.liftArgument_smooth line 412
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.liftedHamiltonian_smooth line 417
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.liftArgument_fderiv line 421
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.liftedHamiltonian_fderiv line 429
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.hamiltonian_slice_fderiv line 438
  23. def OAI.PackingSufficiencySupport.Hamiltonian.liftedAngularSpeed line 445
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.liftedAngularSpeed_smooth line 449
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.liftedHamiltonian_fderiv_inner line 455
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.liftedHamiltonian_fderiv_outer line 462
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.liftedHamiltonian_field line 476