OAI/Geometry/BallPacking/Flows/FlowSmoothExtension.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.flow_smooth_of_uniform_local line 15
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_smooth_global_manifold_flow line 63
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_smooth_global_manifold_flow_of_uniform_families line 106
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_uniform_smooth_manifold_families_of_background line 156
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_smooth_scalar_clock_flow line 200
  6. def OAI.PackingSufficiencySupport.Hamiltonian.timeLiftField line 227
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeLiftField_smooth line 231
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeLiftField_clock_derivative line 250
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeLiftField_spatial_derivative line 266
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeLift_constant_spatial_curve line 286
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeLift_spatial_stationary line 306
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.scalar_clock_eq line 325
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_spatially_compact_time_lift line 350
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_compact_time_lift line 436