OAI/Analysis/LienardCycles/ActualError.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.QuinticLienard.ActualCharacteristic.j line 21
2. def OAI.QuinticLienard.ActualCharacteristic.err line 22
3. def OAI.QuinticLienard.ActualCharacteristic.coeff line 23
4. def OAI.QuinticLienard.ActualCharacteristic.label line 24
5. lemma OAI.QuinticLienard.ActualCharacteristic.j_analytic line 25
6. lemma OAI.QuinticLienard.ActualCharacteristic.j_spec line 28
7. lemma OAI.QuinticLienard.ActualCharacteristic.j_deriv line 30
8. lemma OAI.QuinticLienard.ActualCharacteristic.err_deriv line 60
9. lemma OAI.QuinticLienard.ActualCharacteristic.coeff_pos line 64
10. lemma OAI.QuinticLienard.ActualCharacteristic.coeff_continuous line 66
11. lemma OAI.QuinticLienard.ActualCharacteristic.err_tendsto line 73
12. lemma OAI.QuinticLienard.ActualCharacteristic.label_analytic line 79
13. lemma OAI.QuinticLienard.ActualCharacteristic.label_spec line 82
14. lemma OAI.QuinticLienard.ActualCharacteristic.label_J line 85
15. lemma OAI.QuinticLienard.ActualCharacteristic.label_deriv line 92