OAI/Analysis/LienardCycles/ProfileDerivatives.lean
12 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.QuinticLienard.ScaledProfile.root_posline 20 - lemma
OAI.QuinticLienard.ScaledProfile.root_sqline 21 - lemma
OAI.QuinticLienard.ScaledProfile.root_analyticline 22 - lemma
OAI.QuinticLienard.ScaledProfile.root_hasDerivAtline 24 - lemma
OAI.QuinticLienard.ScaledProfile.poly_hasDerivAtline 30 - lemma
OAI.QuinticLienard.ScaledProfile.cā_hasDerivAtline 39 - lemma
OAI.QuinticLienard.ScaledProfile.cā_hasDerivAtline 47 - lemma
OAI.QuinticLienard.ScaledProfile.profile_hasDerivAtline 54 - lemma
OAI.QuinticLienard.ScaledProfile.slope_hasDerivAtline 57 - lemma
OAI.QuinticLienard.ScaledProfile.curvature_hasDerivAtline 64 - lemma
OAI.QuinticLienard.ScaledProfile.slope_analyticline 76 - lemma
OAI.QuinticLienard.ScaledProfile.curvature_analyticline 80