OAI/Analysis/PathSelection/AnalyticCharts.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Analytic Puiseux charts, zero leading data and clock perturbation estimates.

  1. lemma OAI.DegeneratingTrees.Clock.PositiveSectorControl.tendsto line 16
  2. theorem OAI.DegeneratingTrees.Clock.PuiseuxSector.analytic_change_clock line 40
  3. lemma OAI.DegeneratingTrees.Clock.real_equivalent_of_relative line 137
  4. lemma OAI.DegeneratingTrees.Clock.Puiseux.log_littleO_unbounded line 154
  5. lemma OAI.DegeneratingTrees.Clock.ExpSmall.common_sector_bound line 170
  6. theorem OAI.DegeneratingTrees.Clock.ExpansionOver.zero_leading_data line 192
  7. theorem OAI.DegeneratingTrees.Clock.ExpansionOver.zero_leading_strip_data line 247
  8. theorem OAI.DegeneratingTrees.Clock.analytic_perturbative_inverse line 307
  9. lemma OAI.DegeneratingTrees.Clock.closedBall_inside_double line 386
  10. lemma OAI.DegeneratingTrees.Clock.cauchy_deriv_inner_disc line 392
  11. lemma OAI.DegeneratingTrees.Clock.cauchy_increment_inner_disc line 402
  12. theorem OAI.DegeneratingTrees.Clock.analytic_inverse_of_disc_error line 414