OAI/Analysis/LienardCycles/QuadraticSlices.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.QuinticLienard.QuadraticCoordinates.fderiv_model line 21
  2. lemma OAI.QuinticLienard.QuadraticCoordinates.slice_d line 30
  3. lemma OAI.QuinticLienard.QuadraticCoordinates.slice_k line 35
  4. lemma OAI.QuinticLienard.QuadraticCoordinates.v_translation line 41
  5. lemma OAI.QuinticLienard.QuadraticCoordinates.height_derivative line 51
  6. def OAI.QuinticLienard.QuadraticCoordinates.gap line 62
  7. def OAI.QuinticLienard.QuadraticCoordinates.alpha line 63
  8. def OAI.QuinticLienard.QuadraticCoordinates.gamma line 64
  9. lemma OAI.QuinticLienard.QuadraticCoordinates.width_identity line 67
  10. lemma OAI.QuinticLienard.QuadraticCoordinates.transport_H line 82
  11. lemma OAI.QuinticLienard.QuadraticCoordinates.euler_identity line 89
  12. lemma OAI.QuinticLienard.QuadraticCoordinates.Hr_d_hasDerivAt line 110
  13. lemma OAI.QuinticLienard.QuadraticCoordinates.Hr_k_hasDerivAt line 118
  14. def OAI.QuinticLienard.QuadraticCoordinates.Hrr line 126
  15. lemma OAI.QuinticLienard.QuadraticCoordinates.Hrr_hasDerivAt line 127
  16. lemma OAI.QuinticLienard.QuadraticCoordinates.v_height_derivative line 131
  17. lemma OAI.QuinticLienard.QuadraticCoordinates.v_width_derivative line 142
  18. lemma OAI.QuinticLienard.QuadraticCoordinates.transport_Hr line 152