OAI/Analysis/LienardCycles/QuadraticCoordinates.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuinticLienard.QuadraticCoordinates.H line 20
  2. def OAI.QuinticLienard.QuadraticCoordinates.P line 21
  3. def OAI.QuinticLienard.QuadraticCoordinates.Q line 22
  4. def OAI.QuinticLienard.QuadraticCoordinates.Hr line 23
  5. def OAI.QuinticLienard.QuadraticCoordinates.R line 24
  6. def OAI.QuinticLienard.QuadraticCoordinates.S line 25
  7. def OAI.QuinticLienard.QuadraticCoordinates.G line 26
  8. lemma OAI.QuinticLienard.QuadraticCoordinates.H_analytic line 28
  9. lemma OAI.QuinticLienard.QuadraticCoordinates.P_analytic line 32
  10. lemma OAI.QuinticLienard.QuadraticCoordinates.Q_analytic line 34
  11. lemma OAI.QuinticLienard.QuadraticCoordinates.Hr_analytic line 36
  12. lemma OAI.QuinticLienard.QuadraticCoordinates.R_analytic line 38
  13. lemma OAI.QuinticLienard.QuadraticCoordinates.S_analytic line 40
  14. lemma OAI.QuinticLienard.QuadraticCoordinates.P_hasDerivAt line 43
  15. lemma OAI.QuinticLienard.QuadraticCoordinates.Q_hasDerivAt line 48
  16. lemma OAI.QuinticLienard.QuadraticCoordinates.Hr_hasDerivAt line 53
  17. lemma OAI.QuinticLienard.QuadraticCoordinates.Hr_abs_lt line 58
  18. lemma OAI.QuinticLienard.QuadraticCoordinates.H_abs_lt line 62
  19. lemma OAI.QuinticLienard.QuadraticCoordinates.H_gap_pos line 65
  20. lemma OAI.QuinticLienard.QuadraticCoordinates.translation line 68
  21. lemma OAI.QuinticLienard.QuadraticCoordinates.scaling line 76
  22. lemma OAI.QuinticLienard.QuadraticCoordinates.reflection line 83
  23. lemma OAI.QuinticLienard.QuadraticCoordinates.parabolic_arch line 89
  24. lemma OAI.QuinticLienard.QuadraticCoordinates.zero_data line 115