OAI/Analysis/PathSelection/RecursiveClocks.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Recursive clock monomials, leading terms and coefficient-field algebra.

  1. def OAI.DegeneratingTrees.Clock.ClockGerm line 18
  2. def OAI.DegeneratingTrees.Clock.ValidClocks line 28
  3. lemma OAI.DegeneratingTrees.Clock.ClockGerm.congr line 36
  4. lemma OAI.DegeneratingTrees.Clock.eventually_analytic_congr line 44
  5. theorem OAI.DegeneratingTrees.Clock.ClockGerm.eventually_analytic line 53
  6. lemma OAI.DegeneratingTrees.Clock.ClockGerm.real_eventually_analytic line 68
  7. inductive OAI.DegeneratingTrees.Clock.LogMonomial line 76
  8. def OAI.DegeneratingTrees.Clock.RayLeading line 81
  9. lemma OAI.DegeneratingTrees.Clock.continuous_tail_surjective line 87
  10. lemma OAI.DegeneratingTrees.Clock.eventually_of_comp_clock line 100
  11. lemma OAI.DegeneratingTrees.Clock.ValidClocks.lower_small line 121
  12. lemma OAI.DegeneratingTrees.Clock.LogMonomial.isLittleO line 138
  13. lemma OAI.DegeneratingTrees.Clock.LogMonomial.neg line 147
  14. lemma OAI.DegeneratingTrees.Clock.subexponential_exp_of_littleO line 157
  15. lemma OAI.DegeneratingTrees.Clock.subexponential_of_eventually_bounded line 167
  16. lemma OAI.DegeneratingTrees.Clock.subexponential_congr line 176
  17. lemma OAI.DegeneratingTrees.Clock.RayLeading.inv line 182
  18. lemma OAI.DegeneratingTrees.Clock.RayLeading.eventually_nonzero line 190
  19. lemma OAI.DegeneratingTrees.Clock.RayLeading.subexponential line 196
  20. lemma OAI.DegeneratingTrees.Clock.RayLeading.eventually_sign line 211
  21. lemma OAI.DegeneratingTrees.Clock.Puiseux.rayLeading line 232
  22. theorem OAI.DegeneratingTrees.Clock.ClockGerm.leading_or_zero line 256
  23. lemma OAI.DegeneratingTrees.Clock.ClockGerm.leading line 306
  24. lemma OAI.DegeneratingTrees.Clock.ClockGerm.eventually_nonzero line 310
  25. theorem OAI.DegeneratingTrees.Clock.ClockGerm.eventually_sign line 316
  26. lemma OAI.DegeneratingTrees.Clock.ClockGerm.const line 336
  27. lemma OAI.DegeneratingTrees.Clock.ClockGerm.neg line 344
  28. lemma OAI.DegeneratingTrees.Clock.ClockGerm.add line 354
  29. lemma OAI.DegeneratingTrees.Clock.ClockGerm.sub line 379
  30. lemma OAI.DegeneratingTrees.Clock.puiseux_of_comp_clock line 394
  31. lemma OAI.DegeneratingTrees.Clock.firstClock_expansion_iff line 400
  32. lemma OAI.DegeneratingTrees.Clock.ClockGerm.first_mul line 412
  33. lemma OAI.DegeneratingTrees.Clock.ClockGerm.first_inv line 421