OAI/Geometry/BallPacking/Moser/ManifoldExteriorNaturality.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.euclideanPullback_exact_time line 18
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldPullback_exact_time line 56
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.chart_averageOneForm_fderiv line 92
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothCircleAction.averaged_moser_data line 111
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.nonautonomous_curve_lift line 150
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.nonautonomous_curve_eqOn line 165
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.related_nonautonomous_curve line 195
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.related_nonautonomous_flow line 216
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.compact_related_flow_preserves_range line 239
  10. def OAI.PackingSufficiencySupport.Hamiltonian.reparametrizedTimeField line 272
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.reparametrizedTimeField_smooth line 276
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.reparametrizedTimeField_curve line 305
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.nonautonomous_curve_eqOn_Icc line 328
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.related_nonautonomous_flow_Icc line 371
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.compact_related_flow_preserves_range_Icc line 393
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.spatially_compact_flow_preserves_split_range line 428
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_compact_radial_relative_moser line 494
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.cutoff_phaseSq_zero line 595
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.degreeConePrimitive_zero line 597
  20. def OAI.PackingSufficiencySupport.Hamiltonian.cutoffDegreePrimitive line 607
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.cutoffDegreePrimitive_eq line 611
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.cutoffDegreePrimitive_smooth line 617
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.cutoffDegreePrimitive_nhds_zero line 641
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.cutoffDegreePrimitive_slice_smooth line 651
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.cutoffDegreePrimitive_nondegenerate line 665