OAI/Analysis/LienardCycles/Characteristic.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuinticLienard.ReferenceCharacteristic.base line 19
  2. def OAI.QuinticLienard.ReferenceCharacteristic.J line 21
  3. def OAI.QuinticLienard.ReferenceCharacteristic.A line 22
  4. def OAI.QuinticLienard.ReferenceCharacteristic.D line 23
  5. def OAI.QuinticLienard.ReferenceCharacteristic.Jz line 24
  6. def OAI.QuinticLienard.ReferenceCharacteristic.Jk line 25
  7. def OAI.QuinticLienard.ReferenceCharacteristic.Az line 26
  8. def OAI.QuinticLienard.ReferenceCharacteristic.Ak line 27
  9. def OAI.QuinticLienard.ReferenceCharacteristic.Dz line 28
  10. def OAI.QuinticLienard.ReferenceCharacteristic.Dk line 29
  11. lemma OAI.QuinticLienard.ReferenceCharacteristic.base_analytic line 31
  12. lemma OAI.QuinticLienard.ReferenceCharacteristic.J_analytic line 34
  13. lemma OAI.QuinticLienard.ReferenceCharacteristic.A_analytic line 38
  14. lemma OAI.QuinticLienard.ReferenceCharacteristic.D_analytic line 42
  15. lemma OAI.QuinticLienard.ReferenceCharacteristic.Jz_hasDerivAt line 46
  16. lemma OAI.QuinticLienard.ReferenceCharacteristic.Jk_hasDerivAt line 49
  17. lemma OAI.QuinticLienard.ReferenceCharacteristic.Az_hasDerivAt line 52
  18. lemma OAI.QuinticLienard.ReferenceCharacteristic.Ak_hasDerivAt line 55
  19. lemma OAI.QuinticLienard.ReferenceCharacteristic.Dz_hasDerivAt line 58
  20. lemma OAI.QuinticLienard.ReferenceCharacteristic.Dk_hasDerivAt line 61
  21. lemma OAI.QuinticLienard.ReferenceCharacteristic.A_abs_lt line 65
  22. lemma OAI.QuinticLienard.ReferenceCharacteristic.D_abs_lt line 69
  23. lemma OAI.QuinticLienard.ReferenceCharacteristic.A_gap_pos line 70
  24. lemma OAI.QuinticLienard.ReferenceCharacteristic.D_gap_pos line 73
  25. lemma OAI.QuinticLienard.ReferenceCharacteristic.base_deriv line 77
  26. lemma OAI.QuinticLienard.ReferenceCharacteristic.J_deriv line 86
  27. lemma OAI.QuinticLienard.ReferenceCharacteristic.A_deriv line 91
  28. lemma OAI.QuinticLienard.ReferenceCharacteristic.D_deriv line 107