OAI/Analysis/LienardCycles/SharpReturn.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.QuinticLienard.Sharpness.turn line 23
2. lemma OAI.QuinticLienard.Sharpness.turn_pos line 24
3. def OAI.QuinticLienard.Sharpness.initial line 25
4. structure OAI.QuinticLienard.Sharpness.ReturnFamily line 26
5. def OAI.QuinticLienard.Sharpness.ReturnFamily.path line 33
6. def OAI.QuinticLienard.Sharpness.ReturnFamily.Q line 35
7. lemma OAI.QuinticLienard.Sharpness.ReturnFamily.continuous line 36
8. lemma OAI.QuinticLienard.Sharpness.ReturnFamily.path_zero line 38
9. lemma OAI.QuinticLienard.Sharpness.ReturnFamily.deriv line 39
10. lemma OAI.QuinticLienard.Sharpness.return_family line 41