OAI/Analysis/LienardCycles/EndpointJets.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuinticLienard.ModelEndpoint.Xj line 19
  2. def OAI.QuinticLienard.ModelEndpoint.Xjj line 20
  3. def OAI.QuinticLienard.ModelEndpoint.Zj line 21
  4. def OAI.QuinticLienard.ModelEndpoint.Zjj line 22
  5. def OAI.QuinticLienard.ModelEndpoint.gj line 23
  6. def OAI.QuinticLienard.ModelEndpoint.gjj line 24
  7. def OAI.QuinticLienard.ModelEndpoint.gr line 25
  8. def OAI.QuinticLienard.ModelEndpoint.grr line 26
  9. lemma OAI.QuinticLienard.ModelEndpoint.endpoint_identities line 28
  10. lemma OAI.QuinticLienard.ModelEndpoint.m_deriv line 51
  11. lemma OAI.QuinticLienard.ModelEndpoint.n_deriv line 54
  12. lemma OAI.QuinticLienard.ModelEndpoint.ell_deriv_scaled line 59
  13. lemma OAI.QuinticLienard.ModelEndpoint.w_deriv_scaled line 68
  14. lemma OAI.QuinticLienard.ModelEndpoint.endpoint_first_derivs line 72
  15. lemma OAI.QuinticLienard.ModelEndpoint.endpoint_second_derivs line 86
  16. lemma OAI.QuinticLienard.ModelEndpoint.gamma_analytic line 100
  17. lemma OAI.QuinticLienard.ModelEndpoint.gr_analytic line 106
  18. lemma OAI.QuinticLienard.ModelEndpoint.gr_deriv line 108
  19. lemma OAI.QuinticLienard.ModelEndpoint.grr_deriv line 111
  20. lemma OAI.QuinticLienard.ModelEndpoint.first_jets line 115
  21. lemma OAI.QuinticLienard.ModelEndpoint.second_jets line 135
  22. lemma OAI.QuinticLienard.ModelEndpoint.Xj_pos line 157
  23. lemma OAI.QuinticLienard.ModelEndpoint.determinant_W line 161