OAI/Geometry/PolarProducts/LocalODE.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SmoothODE.Time line 18
  2. def OAI.SmoothODE.extend line 24
  3. theorem OAI.SmoothODE.continuous_extend line 27
  4. theorem OAI.SmoothODE.extend_coe line 31
  5. def OAI.SmoothODE.primitive line 34
  6. theorem OAI.SmoothODE.primitive_apply line 39
  7. theorem OAI.SmoothODE.norm_primitive_le line 42
  8. def OAI.SmoothODE.primitiveCLM line 53
  9. theorem OAI.SmoothODE.primitiveCLM_apply line 72
  10. theorem OAI.SmoothODE.primitiveCLM_norm_le line 74
  11. def OAI.SmoothODE.picard line 91
  12. theorem OAI.SmoothODE.lipschitz_superpose line 96
  13. theorem OAI.SmoothODE.lipschitz_picard line 107
  14. theorem OAI.SmoothODE.contDiff_picard line 119
  15. def OAI.SmoothODE.trajectory line 128
  16. theorem OAI.SmoothODE.trajectory_eq line 132
  17. theorem OAI.SmoothODE.contDiff_trajectory line 137
  18. def OAI.SmoothODE.curve line 142
  19. theorem OAI.SmoothODE.curve_coe line 146
  20. theorem OAI.SmoothODE.curve_zero line 151
  21. theorem OAI.SmoothODE.continuous_curve line 155
  22. theorem OAI.SmoothODE.hasDerivAt_curve line 161
  23. def OAI.SmoothODE.step line 174
  24. theorem OAI.SmoothODE.contDiff_step line 178
  25. theorem OAI.SmoothODE.curve_one line 184
  26. theorem OAI.SmoothODE.curve_unique line 201
  27. theorem OAI.SmoothODE.curve_reverse line 220
  28. theorem OAI.SmoothODE.step_neg_step line 236
  29. def OAI.SmoothODE.stepHomeomorph line 242
  30. theorem OAI.SmoothODE.stepHomeomorph_apply line 253
  31. theorem OAI.SmoothODE.curve_of_eq_zero line 258
  32. theorem OAI.SmoothODE.step_of_eq_zero line 267
  33. def OAI.SmoothODE.tangentPath line 286
  34. theorem OAI.SmoothODE.tangentPath_eq line 290