OAI/Analysis/LienardCycles/ActualCharacteristic.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuinticLienard.ActualCharacteristic.b line 21
  2. def OAI.QuinticLienard.ActualCharacteristic.Adm line 22
  3. def OAI.QuinticLienard.ActualCharacteristic.point line 23
  4. def OAI.QuinticLienard.ActualCharacteristic.m line 24
  5. def OAI.QuinticLienard.ActualCharacteristic.v line 25
  6. def OAI.QuinticLienard.ActualCharacteristic.A line 26
  7. def OAI.QuinticLienard.ActualCharacteristic.g line 27
  8. def OAI.QuinticLienard.ActualCharacteristic.k line 28
  9. def OAI.QuinticLienard.ActualCharacteristic.c line 29
  10. lemma OAI.QuinticLienard.ActualCharacteristic.base_spec line 30
  11. lemma OAI.QuinticLienard.ActualCharacteristic.radius_pos line 33
  12. lemma OAI.QuinticLienard.ActualCharacteristic.m_abs_lt line 35
  13. lemma OAI.QuinticLienard.ActualCharacteristic.v_abs_lt line 37
  14. lemma OAI.QuinticLienard.ActualCharacteristic.A_abs_lt line 39
  15. lemma OAI.QuinticLienard.ActualCharacteristic.g_pos line 43
  16. lemma OAI.QuinticLienard.ActualCharacteristic.base_analytic line 45
  17. lemma OAI.QuinticLienard.ActualCharacteristic.adm_eventually line 48
  18. lemma OAI.QuinticLienard.ActualCharacteristic.point_analytic line 51
  19. lemma OAI.QuinticLienard.ActualCharacteristic.m_analytic line 53
  20. lemma OAI.QuinticLienard.ActualCharacteristic.v_analytic line 55
  21. lemma OAI.QuinticLienard.ActualCharacteristic.A_analytic line 57
  22. lemma OAI.QuinticLienard.ActualCharacteristic.k_analytic line 59
  23. lemma OAI.QuinticLienard.ActualCharacteristic.c_analytic line 61
  24. lemma OAI.QuinticLienard.ActualCharacteristic.base_deriv line 63
  25. lemma OAI.QuinticLienard.ActualCharacteristic.along_deriv line 69
  26. lemma OAI.QuinticLienard.ActualCharacteristic.m_deriv line 78
  27. lemma OAI.QuinticLienard.ActualCharacteristic.v_deriv line 90
  28. lemma OAI.QuinticLienard.ActualCharacteristic.A_deriv line 99
  29. lemma OAI.QuinticLienard.ActualCharacteristic.k_deriv line 105
  30. lemma OAI.QuinticLienard.ActualCharacteristic.c_deriv line 109
  31. def OAI.QuinticLienard.ActualCharacteristic.L line 113
  32. def OAI.QuinticLienard.ActualCharacteristic.rate line 114
  33. lemma OAI.QuinticLienard.ActualCharacteristic.L_deriv line 115
  34. lemma OAI.QuinticLienard.ActualCharacteristic.adm_le line 123
  35. lemma OAI.QuinticLienard.ActualCharacteristic.base_tendsto line 128
  36. lemma OAI.QuinticLienard.ActualCharacteristic.small_limits line 131