OAI/Analysis/PathSelection/PositiveCharts.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Positive clock charts, power sectors and changes of Puiseux clock.

  1. def OAI.DegeneratingTrees.Clock.PositiveExponentialChart line 16
  2. lemma OAI.DegeneratingTrees.Clock.normalized_leading_nonzero line 33
  3. lemma OAI.DegeneratingTrees.Clock.ExpSmall.strip_bound line 42
  4. lemma OAI.DegeneratingTrees.Clock.real_positive_quotient line 50
  5. theorem OAI.DegeneratingTrees.Clock.ExpansionOver.first_positive_chart line 62
  6. theorem OAI.DegeneratingTrees.Clock.ExpansionOver.positive_chart line 176
  7. theorem OAI.DegeneratingTrees.Clock.power_model_linear_sector line 289
  8. lemma OAI.DegeneratingTrees.Clock.power_exponent_le_one line 361
  9. lemma OAI.DegeneratingTrees.Clock.power_exponent_lt_one line 379
  10. theorem OAI.DegeneratingTrees.Clock.Puiseux.sector_control line 406
  11. def OAI.DegeneratingTrees.Clock.PositiveSectorControl line 465
  12. theorem OAI.DegeneratingTrees.Clock.Puiseux.change_clock line 476