OAI/Analysis/LienardCycles/ScalarArcs.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.QuinticLienard.ScalarArcs.bounded_profile_solution line 16
  2. lemma OAI.QuinticLienard.ScalarArcs.weighted_strictAnti line 69
  3. theorem OAI.QuinticLienard.ScalarArcs.derivative_signs line 81
  4. lemma OAI.QuinticLienard.ScalarArcs.branch_monotonicity line 105
  5. theorem OAI.QuinticLienard.ScalarArcs.endpoints line 121
  6. theorem OAI.QuinticLienard.ScalarArcs.positive_profile_extension line 183
  7. theorem OAI.QuinticLienard.ScalarArcs.entire_profile_extension line 217
  8. structure OAI.QuinticLienard.ScalarArcs.IsArch line 236
  9. lemma OAI.QuinticLienard.ScalarArcs.arch_of_extension line 250
  10. theorem OAI.QuinticLienard.ScalarArcs.positive_arch_exists line 278
  11. theorem OAI.QuinticLienard.ScalarArcs.entire_arch_exists line 284
  12. theorem OAI.QuinticLienard.ScalarArcs.IsArch.unique line 290
  13. def OAI.QuinticLienard.ScalarArcs.archTuple line 358
  14. def OAI.QuinticLienard.ScalarArcs.archFunction line 361
  15. def OAI.QuinticLienard.ScalarArcs.lower line 362
  16. def OAI.QuinticLienard.ScalarArcs.upper line 363
  17. def OAI.QuinticLienard.ScalarArcs.width line 364
  18. def OAI.QuinticLienard.ScalarArcs.midpoint line 365
  19. theorem OAI.QuinticLienard.ScalarArcs.chosen_arch line 368
  20. theorem OAI.QuinticLienard.ScalarArcs.midpoint_abs_lt_width line 375
  21. lemma OAI.QuinticLienard.ScalarArcs.derivative_signs_on_Icc line 383
  22. theorem OAI.QuinticLienard.ScalarArcs.IsArch.of_solution_and_hits line 424
  23. theorem OAI.QuinticLienard.ScalarArcs.IsArch.subarch line 459