OAI/Analysis/LienardCycles/ScaledAlgebraic.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.QuinticLienard.ScaledProfile.Params line 19
  2. abbrev OAI.QuinticLienard.ScaledProfile.Dom line 20
  3. def OAI.QuinticLienard.ScaledProfile.A line 21
  4. def OAI.QuinticLienard.ScaledProfile.ρ line 24
  5. def OAI.QuinticLienard.ScaledProfile.ε line 27
  6. def OAI.QuinticLienard.ScaledProfile.s line 29
  7. def OAI.QuinticLienard.ScaledProfile.X line 30
  8. def OAI.QuinticLienard.ScaledProfile.Z line 31
  9. def OAI.QuinticLienard.ScaledProfile.Δ line 32
  10. def OAI.QuinticLienard.ScaledProfile.C₁ line 33
  11. def OAI.QuinticLienard.ScaledProfile.C₂ line 35
  12. def OAI.QuinticLienard.ScaledProfile.C₃ line 37
  13. def OAI.QuinticLienard.ScaledProfile.C₄ line 39
  14. def OAI.QuinticLienard.ScaledProfile.K line 41
  15. def OAI.QuinticLienard.ScaledProfile.B line 42
  16. def OAI.QuinticLienard.ScaledProfile.Rem line 44
  17. def OAI.QuinticLienard.ScaledProfile.η line 48
  18. def OAI.QuinticLienard.ScaledProfile.Expr line 49
  19. def OAI.QuinticLienard.ScaledProfile.Φ line 51
  20. lemma OAI.QuinticLienard.ScaledProfile.eval_A line 53
  21. lemma OAI.QuinticLienard.ScaledProfile.eval_ρ line 54
  22. lemma OAI.QuinticLienard.ScaledProfile.eval_ε line 55
  23. lemma OAI.QuinticLienard.ScaledProfile.eval_s line 56
  24. lemma OAI.QuinticLienard.ScaledProfile.regular_A line 57
  25. lemma OAI.QuinticLienard.ScaledProfile.regular_ρ line 58
  26. lemma OAI.QuinticLienard.ScaledProfile.regular_ε line 59
  27. lemma OAI.QuinticLienard.ScaledProfile.regular_s line 60
  28. lemma OAI.QuinticLienard.ScaledProfile.X_pos line 61
  29. lemma OAI.QuinticLienard.ScaledProfile.Z_pos line 65
  30. lemma OAI.QuinticLienard.ScaledProfile.X_regular line 69
  31. lemma OAI.QuinticLienard.ScaledProfile.Z_regular line 74
  32. lemma OAI.QuinticLienard.ScaledProfile.regular line 79
  33. lemma OAI.QuinticLienard.ScaledProfile.analytic line 93
  34. lemma OAI.QuinticLienard.ScaledProfile.local_flow line 95
  35. lemma OAI.QuinticLienard.ScaledProfile.base_zero line 100
  36. lemma OAI.QuinticLienard.ScaledProfile.rho_zero line 102