OAI/Analysis/LienardCycles/CycleSection.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.QuinticLienard.solution_unique_Icc line 23
  2. lemma OAI.QuinticLienard.IsPeriodicOrbit.positive_axis line 39
  3. lemma OAI.QuinticLienard.IsPeriodicOrbit.axis_unique line 46
  4. lemma OAI.QuinticLienard.IsPeriodicOrbit.not_equilibrium line 52
  5. lemma OAI.QuinticLienard.IsPeriodicOrbit.limitCycle_of_section line 57
  6. lemma OAI.QuinticLienard.IsPeriodicOrbit.limitCycle_of_return line 87