OAI/Analysis/LienardCycles/HeightSigns.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.QuinticLienard.ModelEndpoint.d_neg_of_H_negline 17 - lemma
OAI.QuinticLienard.ModelEndpoint.Hr_pos_of_H_nonnegline 32 - lemma
OAI.QuinticLienard.ModelEndpoint.w_pos_of_H_nonnegline 41 - lemma
OAI.QuinticLienard.ModelEndpoint.sch_pos_of_H_neg_Hr_nonnegline 61 - lemma
OAI.QuinticLienard.ModelEndpoint.w_nonneg_of_H_neg_Hr_nonnegline 83