OAI/Analysis/LienardCycles/Riccati.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.QuinticLienard.Riccati.inverse_square_integral_bound line 19
2. def OAI.QuinticLienard.Riccati.multiplier line 70
3. lemma OAI.QuinticLienard.Riccati.multiplier_pos line 73
4. lemma OAI.QuinticLienard.Riccati.multiplier_initial line 76
5. lemma OAI.QuinticLienard.Riccati.multiplier_deriv line 79
6. theorem OAI.QuinticLienard.Riccati.multiplier_second_deriv line 87
7. theorem OAI.QuinticLienard.Riccati.quadratic_inverse_square_bound line 96
8. theorem OAI.QuinticLienard.Riccati.endpoint_variation_bound line 130