OAI/Analysis/LienardCycles/SharpFlow.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.QuinticLienard.Sharpness.Space line 23
  2. def OAI.QuinticLienard.Sharpness.f line 24
  3. def OAI.QuinticLienard.Sharpness.V line 25
  4. def OAI.QuinticLienard.Sharpness.X line 26
  5. def OAI.QuinticLienard.Sharpness.Eps line 27
  6. def OAI.QuinticLienard.Sharpness.polynomial line 28
  7. lemma OAI.QuinticLienard.Sharpness.polynomial_eval line 29
  8. lemma OAI.QuinticLienard.Sharpness.polynomial_regular line 30
  9. lemma OAI.QuinticLienard.Sharpness.field_contDiff line 31
  10. lemma OAI.QuinticLienard.Sharpness.local_flow line 32
  11. def OAI.QuinticLienard.Sharpness.I2 line 50
  12. def OAI.QuinticLienard.Sharpness.I4 line 51
  13. def OAI.QuinticLienard.Sharpness.I6 line 52
  14. lemma OAI.QuinticLienard.Sharpness.deriv_I2 line 53
  15. lemma OAI.QuinticLienard.Sharpness.deriv_I4 line 57
  16. lemma OAI.QuinticLienard.Sharpness.deriv_I6 line 65
  17. def OAI.QuinticLienard.Sharpness.q line 73
  18. lemma OAI.QuinticLienard.Sharpness.deriv_q line 74
  19. def OAI.QuinticLienard.Sharpness.circle line 78
  20. lemma OAI.QuinticLienard.Sharpness.circle_deriv line 79
  21. lemma OAI.QuinticLienard.Sharpness.circle_zero line 82
  22. lemma OAI.QuinticLienard.Sharpness.q_turn line 83
  23. lemma OAI.QuinticLienard.Sharpness.circle_continuous line 85