OAI/Analysis/LienardCycles/SharpPhysical.lean
13 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.QuinticLienard.Sharpness.Fline 23 - lemma
OAI.QuinticLienard.Sharpness.F_evalline 25 - lemma
OAI.QuinticLienard.Sharpness.F_zeroline 26 - lemma
OAI.QuinticLienard.Sharpness.F_degreeline 27 - def
OAI.QuinticLienard.Sharpness.projectline 28 - lemma
OAI.QuinticLienard.Sharpness.eps_derivline 29 - lemma
OAI.QuinticLienard.Sharpness.xy_derivline 32 - lemma
OAI.QuinticLienard.Sharpness.q_derivline 35 - lemma
OAI.QuinticLienard.Sharpness.eps_constantline 39 - lemma
OAI.QuinticLienard.Sharpness.energy_identityline 45 - lemma
OAI.QuinticLienard.Sharpness.ReturnFamily.physical_derivline 66 - lemma
OAI.QuinticLienard.Sharpness.ReturnFamily.closed_of_Qline 73 - lemma
OAI.QuinticLienard.Sharpness.ReturnFamily.periodic_orbitline 86