OAI/Geometry/BallPacking/Moser/RelativeForms.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.smooth_fixedPoint line 14
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.smoothOn_contraction_solution line 49
  3. def OAI.PackingSufficiencySupport.Hamiltonian.pathLinear line 96
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.pathLinear_apply line 108
  5. def OAI.PackingSufficiencySupport.Hamiltonian.pathLinearOperator line 111
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.pathLinearOperator_apply line 127
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.uniform_taylor line 130
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.postcomp_hasFDerivAt line 156
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.postcomp_contDiff_nat line 173
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.postcomp_contDiff line 187
  11. abbrev OAI.PackingSufficiencySupport.Hamiltonian.Time line 202
  12. def OAI.PackingSufficiencySupport.Hamiltonian.extendPath line 204
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.extendPath_coe line 208
  14. def OAI.PackingSufficiencySupport.Hamiltonian.pathIntegral line 212
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.pathIntegral_apply line 237
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.pathIntegral_zero line 240
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.norm_pathIntegral_le line 243
  18. def OAI.PackingSufficiencySupport.Hamiltonian.constantPath line 254
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.constantPath_apply line 267
  20. def OAI.PackingSufficiencySupport.Hamiltonian.picard line 269
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.picard_apply line 272
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.postcomp_lipschitz line 276
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.picard_lipschitz line 285
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.picard_contDiff line 296
  25. def OAI.PackingSufficiencySupport.Hamiltonian.picardDomain line 303
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.picardDomain_open line 306
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.picard_contracts line 309
  28. def OAI.PackingSufficiencySupport.Hamiltonian.localPath line 314
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.localPath_fixed line 319
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.localPath_smooth line 325
  31. def OAI.PackingSufficiencySupport.Hamiltonian.fixedStep line 333
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.fixedStep_smooth line 336
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.fixedStep_equation line 345
  34. theorem OAI.PackingSufficiencySupport.Hamiltonian.fixedStep_initial line 350
  35. theorem OAI.PackingSufficiencySupport.Hamiltonian.fixedStep_variation line 356
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.path_equation_derivative line 377
  37. theorem OAI.PackingSufficiencySupport.Hamiltonian.fixedStep_derivative line 393
  38. def OAI.PackingSufficiencySupport.Hamiltonian.stepEndpoint line 399
  39. theorem OAI.PackingSufficiencySupport.Hamiltonian.stepEndpoint_smooth line 402
  40. theorem OAI.PackingSufficiencySupport.Hamiltonian.stepEndpoint_injective line 408
  41. theorem OAI.PackingSufficiencySupport.Hamiltonian.stepEndpoint_fderiv line 438
  42. theorem OAI.PackingSufficiencySupport.Hamiltonian.stepEndpoint_preserves_bilinear line 447
  43. def OAI.PackingSufficiencySupport.Hamiltonian.reverseTime line 500
  44. def OAI.PackingSufficiencySupport.Hamiltonian.reversePath line 503
  45. theorem OAI.PackingSufficiencySupport.Hamiltonian.reversePath_integral line 507
  46. theorem OAI.PackingSufficiencySupport.Hamiltonian.fixedStep_reverse line 526
  47. theorem OAI.PackingSufficiencySupport.Hamiltonian.stepEndpoint_neg_leftInverse line 550