OAI/Analysis/LienardCycles/PartialCalculus.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuinticLienard.PartialCalculus.direction line 20
  2. lemma OAI.QuinticLienard.PartialCalculus.direction_contDiffAt line 22
  3. lemma OAI.QuinticLienard.PartialCalculus.direction_hasFDerivAt line 26
  4. lemma OAI.QuinticLienard.PartialCalculus.direction_direction line 35
  5. lemma OAI.QuinticLienard.PartialCalculus.direction_comm line 40
  6. def OAI.QuinticLienard.PartialCalculus.first line 45
  7. def OAI.QuinticLienard.PartialCalculus.second line 46
  8. lemma OAI.QuinticLienard.PartialCalculus.first_contDiffAt line 48
  9. lemma OAI.QuinticLienard.PartialCalculus.second_contDiffAt line 50
  10. lemma OAI.QuinticLienard.PartialCalculus.first_hasDerivAt line 53
  11. lemma OAI.QuinticLienard.PartialCalculus.second_hasDerivAt line 59
  12. lemma OAI.QuinticLienard.PartialCalculus.mixed_comm line 65
  13. lemma OAI.QuinticLienard.PartialCalculus.fderiv_pair line 68
  14. theorem OAI.QuinticLienard.PartialCalculus.scalar_ode_variation line 74
  15. theorem OAI.QuinticLienard.PartialCalculus.transverse_hit line 101
  16. lemma OAI.QuinticLienard.PartialCalculus.eq_of_hasDerivAt_eq_on_Icc line 125