OAI/Analysis/LienardCycles/CurvatureComparison.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.QuinticLienard.QuadraticCoordinates.transport_W_at_zero line 20
2. lemma OAI.QuinticLienard.QuadraticCoordinates.characteristic_deriv line 29
3. lemma OAI.QuinticLienard.QuadraticCoordinates.W_pos_of_curvature_pos line 43
4. lemma OAI.QuinticLienard.QuadraticCoordinates.P_reflection line 62
5. lemma OAI.QuinticLienard.QuadraticCoordinates.Q_reflection line 67
6. lemma OAI.QuinticLienard.QuadraticCoordinates.R_reflection line 72
7. lemma OAI.QuinticLienard.QuadraticCoordinates.S_reflection line 75
8. lemma OAI.QuinticLienard.QuadraticCoordinates.Rr_reflection line 78
9. lemma OAI.QuinticLienard.QuadraticCoordinates.Sr_reflection line 81
10. lemma OAI.QuinticLienard.QuadraticCoordinates.W_reflection line 84
11. lemma OAI.QuinticLienard.QuadraticCoordinates.W_nonneg line 87
12. lemma OAI.QuinticLienard.QuadraticCoordinates.G_deriv line 99
13. theorem OAI.QuinticLienard.QuadraticCoordinates.model_inequality line 105