OAI/Analysis/LienardCycles/PositiveVariation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.QuinticLienard.PositiveVariation.positive_homogeneous_on line 22
2. lemma OAI.QuinticLienard.PositiveVariation.peak_derivative_positive_local line 35
3. lemma OAI.QuinticLienard.PositiveVariation.endpoints line 63
4. lemma OAI.QuinticLienard.PositiveVariation.endpoint_witness line 72
5. theorem OAI.QuinticLienard.PositiveVariation.peak_signs line 90
6. theorem OAI.QuinticLienard.PositiveVariation.base_derivatives line 138
7. theorem OAI.QuinticLienard.PositiveVariation.peak_width_midpoint_bounds line 183