OAI/Analysis/LienardCycles/ModelAlgebra.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuinticLienard.ModelAlgebra.wStar line 17
  2. def OAI.QuinticLienard.ModelAlgebra.dStar line 20
  3. def OAI.QuinticLienard.ModelAlgebra.schwarzian line 23
  4. def OAI.QuinticLienard.ModelAlgebra.A line 27
  5. def OAI.QuinticLienard.ModelAlgebra.T line 28
  6. def OAI.QuinticLienard.ModelAlgebra.J line 29
  7. def OAI.QuinticLienard.ModelAlgebra.Sā‚€ line 30
  8. lemma OAI.QuinticLienard.ModelAlgebra.A_pos line 32
  9. lemma OAI.QuinticLienard.ModelAlgebra.J_pos line 39
  10. lemma OAI.QuinticLienard.ModelAlgebra.wStar_normalized line 47
  11. lemma OAI.QuinticLienard.ModelAlgebra.wStar_pos line 52
  12. lemma OAI.QuinticLienard.ModelAlgebra.baseline line 63
  13. lemma OAI.QuinticLienard.ModelAlgebra.delta_factor line 73
  14. lemma OAI.QuinticLienard.ModelAlgebra.derivative_at_wStar line 82
  15. lemma OAI.QuinticLienard.ModelAlgebra.dStar_mono_from_wStar line 91
  16. lemma OAI.QuinticLienard.ModelAlgebra.schwarzian_improvement line 108
  17. lemma OAI.QuinticLienard.ModelAlgebra.schwarzian_last line 115
  18. lemma OAI.QuinticLienard.ModelAlgebra.riccati_consequence line 122
  19. lemma OAI.QuinticLienard.ModelAlgebra.last_case_nonneg_T line 129
  20. lemma OAI.QuinticLienard.ModelAlgebra.negative_T_estimates line 167
  21. lemma OAI.QuinticLienard.ModelAlgebra.slope_estimate line 180
  22. lemma OAI.QuinticLienard.ModelAlgebra.last_case_neg_T line 194
  23. lemma OAI.QuinticLienard.ModelAlgebra.last_case line 249
  24. lemma OAI.QuinticLienard.ModelAlgebra.wStar_neg line 260
  25. lemma OAI.QuinticLienard.ModelAlgebra.equal_endpoints_pos line 273
  26. lemma OAI.QuinticLienard.ModelAlgebra.schwarzian_pos_of_one_le line 279
  27. lemma OAI.QuinticLienard.ModelAlgebra.second_case line 296
  28. lemma OAI.QuinticLienard.ModelAlgebra.zero_sign line 312