OAI/Analysis/LienardCycles/Schwarzian.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuinticLienard.ModelEndpoint.w line 20
  2. def OAI.QuinticLienard.ModelEndpoint.sch line 22
  3. lemma OAI.QuinticLienard.ModelEndpoint.Hrr_analytic line 26
  4. lemma OAI.QuinticLienard.ModelEndpoint.ell_analytic line 28
  5. lemma OAI.QuinticLienard.ModelEndpoint.w_analytic line 31
  6. lemma OAI.QuinticLienard.ModelEndpoint.ell_deriv line 39
  7. lemma OAI.QuinticLienard.ModelEndpoint.LowerChart.radius_deriv_eventually line 46
  8. lemma OAI.QuinticLienard.ModelEndpoint.LowerChart.upper_deriv_eventually line 60
  9. lemma OAI.QuinticLienard.ModelEndpoint.LowerChart.second_deriv_eventually line 70
  10. lemma OAI.QuinticLienard.ModelEndpoint.LowerChart.log_deriv_eventually line 78
  11. lemma OAI.QuinticLienard.ModelEndpoint.LowerChart.log_deriv line 86
  12. lemma OAI.QuinticLienard.ModelEndpoint.LowerChart.schwarzian line 91
  13. lemma OAI.QuinticLienard.ModelEndpoint.log_deriv_hasDerivAt line 94
  14. lemma OAI.QuinticLienard.ModelEndpoint.w_deriv line 104