OAI/Geometry/BallPacking/Moser/SmoothManifoldIntegral.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.contMDiff_fixed_integral line 16
  2. structure OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction line 45
  3. def OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.slice line 56
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.slice_smooth line 58
  5. def OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.differential line 61
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.differential_add line 64
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.differential_zero line 72
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.differential_period line 78
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.slice_inverse line 85
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.differential_invertible line 89
  11. def OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.average line 96
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.average_smooth line 101
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.average_invariant line 120
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartOneForm_reconstruct line 141
  15. def OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.averageOneForm line 154
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.pullbackOneForm_continuous line 157
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.chart_averageOneForm line 180
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.averageOneForm_smooth line 191
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.pullbackOneForm_add line 203
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.pullbackOneForm_periodic line 213
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.averageOneForm_invariant line 224
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.contDiffOn_fiber_derivative line 251
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.continuous_at_fixed_fiber_derivative line 264
  24. def OAI.PackingSufficiencySupport.Hamiltonian.timePullbackOneForm line 282
  25. def OAI.PackingSufficiencySupport.Hamiltonian.timePullbackTwoForm line 285
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.timePullbackOneForm_contDiffAt line 289
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.timePullbackTwoForm_contDiffAt line 295
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.timePullbackOneForm_fderiv line 302
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.timePullbackOneForm_exterior line 318
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.timePullbackTwoForm_time line 334
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.timePullback_exact_time line 351
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_localized_manifold_moser_field line 372
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifold_moser_PDE line 432
  34. structure OAI.PackingSufficiencySupport.Hamiltonian.ManifoldMoserData line 476
  35. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_compact_manifold_moser line 496