OAI/Analysis/LienardCycles/RealAnalysis.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.QuinticLienard.RealAnalysis.IsIsolatedZeroOn line 20
2. lemma OAI.QuinticLienard.RealAnalysis.encard_le_two_of_no_three line 23
3. lemma OAI.QuinticLienard.RealAnalysis.middle_zero_not_isolated line 44
4. theorem OAI.QuinticLienard.RealAnalysis.isolated_zero_count line 84
5. lemma OAI.QuinticLienard.RealAnalysis.deriv_nonpos_of_left_min line 93
6. lemma OAI.QuinticLienard.RealAnalysis.positive_of_deriv_pos_at_zero line 104
7. theorem OAI.QuinticLienard.RealAnalysis.at_most_one_zero_of_deriv_pos line 121