OAI/Analysis/LienardCycles/PeriodicBasics.lean
12 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.QuinticLienard.vectorField_contDiffline 21 - lemma
OAI.QuinticLienard.IsSolution.continuousline 24 - lemma
OAI.QuinticLienard.IsSolution.x_derivline 26 - lemma
OAI.QuinticLienard.IsSolution.y_derivline 29 - lemma
OAI.QuinticLienard.IsSolution.eq_of_eqline 32 - lemma
OAI.QuinticLienard.IsSolution.shiftline 41 - lemma
OAI.QuinticLienard.IsSolution.periodic_of_hitline 45 - lemma
OAI.QuinticLienard.equilibrium_solutionline 49 - lemma
OAI.QuinticLienard.IsSolution.avoids_equilibriumline 52 - lemma
OAI.QuinticLienard.IsSolution.axis_transverseline 58 - lemma
OAI.QuinticLienard.IsPeriodicOrbit.isCompactline 62 - lemma
OAI.QuinticLienard.IsSolution.axis_finiteline 67