OAI/Geometry/BallPacking/Layers/SmoothFormTransport.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.smooth_fderiv_apply_const line 14
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.joint_spatial_fderiv line 24
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.joint_time_fderiv line 30
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.joint_flow_variation line 37
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.smooth_flow_form_transport_on line 66
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.planeRotate_comp line 109
  7. def OAI.PackingSufficiencySupport.Hamiltonian.toricFlow line 115
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricFlow_zero line 119
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricFlow_moments line 124
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricAngularSpeed_flow line 130
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricFlow_add line 135
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.phase_rotation_smooth line 145
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.toric_flow_angles_smooth line 156
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricFlow_smooth line 164
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricFlow_time_smooth line 168
  16. def OAI.PackingSufficiencySupport.Hamiltonian.toricFlowHomeomorph line 172
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricFlow_hasDerivAt line 181
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricFlow_symplectic line 192
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.joint_flow_fderiv line 219
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.suspension_form_identity line 227
  21. def OAI.PackingSufficiencySupport.Hamiltonian.toricFunction line 241
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricFunction_smooth line 244
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricFlow_energy_differential line 247
  24. def OAI.PackingSufficiencySupport.Hamiltonian.toricSuspension line 259
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricSuspension_smooth line 262
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricSuspension_fderiv line 270
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricSuspension_pullback line 287
  28. def OAI.PackingSufficiencySupport.Hamiltonian.toricSuspensionInverse line 314
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricSuspensionInverse_smooth line 317
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricSuspensionInverse_left line 326
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricSuspensionInverse_right line 331
  32. def OAI.PackingSufficiencySupport.Hamiltonian.toricSuspensionHomeomorph line 335
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricSuspension_moments line 345
  34. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricSuspensionInverse_moments line 349
  35. def OAI.PackingSufficiencySupport.Hamiltonian.layerOrder line 360
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.layerOrder_apply line 364
  37. theorem OAI.PackingSufficiencySupport.Hamiltonian.layerOrder_symm_apply line 366
  38. def OAI.PackingSufficiencySupport.Hamiltonian.stripChart line 368
  39. theorem OAI.PackingSufficiencySupport.Hamiltonian.stripChart_smooth line 371
  40. theorem OAI.PackingSufficiencySupport.Hamiltonian.stripChart_inverse line 374
  41. def OAI.PackingSufficiencySupport.Hamiltonian.layerChart line 432
  42. theorem OAI.PackingSufficiencySupport.Hamiltonian.layerChart_smooth line 435
  43. def OAI.PackingSufficiencySupport.Hamiltonian.layerForm line 439
  44. theorem OAI.PackingSufficiencySupport.Hamiltonian.layerForm_apply line 448
  45. theorem OAI.PackingSufficiencySupport.Hamiltonian.stripChart_fderiv line 456
  46. theorem OAI.PackingSufficiencySupport.Hamiltonian.layerChart_pullback line 465
  47. theorem OAI.PackingSufficiencySupport.Hamiltonian.layerChart_inverse line 478