OAI/Analysis/LienardCycles/SmoothFlow.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.QuinticLienard.SmoothFlow.UnitInterval line 12
  2. abbrev OAI.QuinticLienard.SmoothFlow.Path line 13
  3. def OAI.QuinticLienard.SmoothFlow.clamp line 15
  4. lemma OAI.QuinticLienard.SmoothFlow.clamp_val line 17
  5. lemma OAI.QuinticLienard.SmoothFlow.continuous_clamp line 20
  6. def OAI.QuinticLienard.SmoothFlow.extend line 25
  7. lemma OAI.QuinticLienard.SmoothFlow.continuous_extend line 28
  8. lemma OAI.QuinticLienard.SmoothFlow.extend_val line 32
  9. lemma OAI.QuinticLienard.SmoothFlow.extend_add line 36
  10. lemma OAI.QuinticLienard.SmoothFlow.extend_smul line 37
  11. def OAI.QuinticLienard.SmoothFlow.primitive line 39
  12. lemma OAI.QuinticLienard.SmoothFlow.primitive_apply line 46
  13. lemma OAI.QuinticLienard.SmoothFlow.norm_primitive_le line 49
  14. def OAI.QuinticLienard.SmoothFlow.primitiveCLM line 59
  15. lemma OAI.QuinticLienard.SmoothFlow.primitiveCLM_apply line 74
  16. def OAI.QuinticLienard.SmoothFlow.constCLM line 76
  17. lemma OAI.QuinticLienard.SmoothFlow.constCLM_apply line 86
  18. theorem OAI.QuinticLienard.SmoothFlow.exists_contDiff_picard line 88
  19. lemma OAI.QuinticLienard.SmoothFlow.extend_const line 130
  20. lemma OAI.QuinticLienard.SmoothFlow.primitive_zero line 132
  21. lemma OAI.QuinticLienard.SmoothFlow.hasDerivAt_extend_primitive line 135
  22. lemma OAI.QuinticLienard.SmoothFlow.picard_initial line 143
  23. lemma OAI.QuinticLienard.SmoothFlow.picard_derivative line 148
  24. def OAI.QuinticLienard.SmoothFlow.reparam line 158
  25. lemma OAI.QuinticLienard.SmoothFlow.reparam_apply line 163
  26. lemma OAI.QuinticLienard.SmoothFlow.dist_reparam_const_le line 166
  27. lemma OAI.QuinticLienard.SmoothFlow.abs_mul_lt_one line 172
  28. lemma OAI.QuinticLienard.SmoothFlow.picard_rescale line 180
  29. theorem OAI.QuinticLienard.SmoothFlow.exists_analytic_local_flow_eventually line 206
  30. theorem OAI.QuinticLienard.SmoothFlow.exists_analytic_local_flow line 284
  31. def OAI.QuinticLienard.SmoothFlow.coordinate line 295
  32. lemma OAI.QuinticLienard.SmoothFlow.coordinate_apply line 299
  33. def OAI.QuinticLienard.SmoothFlow.assemble line 302
  34. lemma OAI.QuinticLienard.SmoothFlow.assemble_apply line 316
  35. def OAI.QuinticLienard.SmoothFlow.scalarPolynomial line 319
  36. lemma OAI.QuinticLienard.SmoothFlow.scalarPolynomial_eval line 323
  37. lemma OAI.QuinticLienard.SmoothFlow.contDiff_scalarPolynomial line 331
  38. theorem OAI.QuinticLienard.SmoothFlow.polynomial_local_flow line 340
  39. inductive OAI.QuinticLienard.SmoothFlow.RationalExpr line 355
  40. def OAI.QuinticLienard.SmoothFlow.RationalExpr.eval line 365
  41. def OAI.QuinticLienard.SmoothFlow.RationalExpr.RegularAt line 372
  42. theorem OAI.QuinticLienard.SmoothFlow.RationalExpr.eval_contDiffAt line 379
  43. theorem OAI.QuinticLienard.SmoothFlow.RationalExpr.regular_eventually line 388
  44. theorem OAI.QuinticLienard.SmoothFlow.RationalExpr.regular_isOpen line 397
  45. def OAI.QuinticLienard.SmoothFlow.RationalExpr.onPaths line 400
  46. lemma OAI.QuinticLienard.SmoothFlow.RationalExpr.inverse_eval line 407
  47. theorem OAI.QuinticLienard.SmoothFlow.RationalExpr.path_properties line 415
  48. theorem OAI.QuinticLienard.SmoothFlow.RationalExpr.local_flow line 455