OAI/Geometry/BallPacking/Hamiltonian/LiftedCompact.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.liftedHamiltonian_compact line 15
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.scaledPlanarHamiltonian_support line 56
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.liftedHamiltonian_support_subset line 79
  4. theorem OAI.PackingSufficiencySupport.Comparison.exists_uniform_variable_modulus line 94
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_smooth_positive_shortening line 123
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_shortening_cutoff line 157
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.scaledUnitFamily_convex line 178
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.scaled_trace_inner_estimate line 195
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_scaled_slice_rearrangement line 217
  10. def OAI.PackingSufficiencySupport.Hamiltonian.trajectoryAngularSpeed line 297
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.trajectoryAngularSpeed_continuous line 301
  12. def OAI.PackingSufficiencySupport.Hamiltonian.trajectoryAngle line 311
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.trajectoryAngle_hasDerivAt line 315
  14. def OAI.PackingSufficiencySupport.Hamiltonian.liftedTrajectory line 322
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.liftedTrajectory_inner line 327
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.liftedTrajectory_moments line 332
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.liftedTrajectory_zero line 340
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.liftedTrajectory_hasDerivAt line 348
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.liftedTrajectory_continuous line 366
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_lifted_endpoint line 370
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.homeomorph_family_inverse_smooth line 394
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.trajectoryAngularSpeed_joint_smooth line 423
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.trajectoryAngle_joint_smooth line 435
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.liftedTrajectory_joint_smooth line 441
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_lifted_isotopy line 463
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_lifted_isotopy_object line 490
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.hamiltonianField_zero_off_support line 515
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_hamiltonian_support_collar line 519
  29. def OAI.PackingSufficiencySupport.Hamiltonian.weightedMoment line 538
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.weightedMoment_smooth line 541
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.weightedMoment_fderiv line 546
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.lifted_field_commutes line 559
  33. theorem OAI.PackingSufficiencySupport.MomentPolytope.scaled_lift_support_below line 581
  34. theorem OAI.PackingSufficiencySupport.MomentPolytope.scaled_lift_face_collars line 608
  35. theorem OAI.PackingSufficiencySupport.MomentPolytope.exists_cartesian_lifted_rearrangement line 632
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.hamiltonianField_add line 687
  37. def OAI.PackingSufficiencySupport.Hamiltonian.reparamHamiltonian line 694
  38. theorem OAI.PackingSufficiencySupport.Hamiltonian.reparamHamiltonian_smooth line 697
  39. theorem OAI.PackingSufficiencySupport.Hamiltonian.reparamHamiltonian_compact line 703
  40. theorem OAI.PackingSufficiencySupport.Hamiltonian.hamiltonianField_reparam line 712
  41. theorem OAI.PackingSufficiencySupport.Hamiltonian.hamiltonian_trajectory_fixed line 734