OAI/Analysis/PathSelection/FirstLevelCharts.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

First-level and lower-sector common clock charts.

  1. def OAI.DegeneratingTrees.Clock.SectorClockChart line 16
  2. theorem OAI.DegeneratingTrees.Clock.ExpansionOver.first_zero_chart line 31
  3. lemma OAI.DegeneratingTrees.Clock.real_quotient_tendsto_zero line 149
  4. lemma OAI.DegeneratingTrees.Clock.PositiveExponentialChart.sector line 163
  5. theorem OAI.DegeneratingTrees.Clock.ExpansionOver.first_level_chart line 205
  6. lemma OAI.DegeneratingTrees.Clock.sector_inverse_unique line 234
  7. def OAI.DegeneratingTrees.Clock.ScalarChartAt line 256
  8. theorem OAI.DegeneratingTrees.Clock.ExpansionOver.first_level_common_chart line 264
  9. structure OAI.DegeneratingTrees.Clock.SectorInverse line 316
  10. structure OAI.DegeneratingTrees.Clock.ScalarSectorChart line 323
  11. def OAI.DegeneratingTrees.Clock.HasSectorCharts line 331
  12. lemma OAI.DegeneratingTrees.Clock.real_positive_bigO line 345
  13. lemma OAI.DegeneratingTrees.Clock.puiseux_hasSectorCharts line 355
  14. def OAI.DegeneratingTrees.Clock.LowerSectorCharts line 376