OAI/Analysis/PathSelection/SectorPolynomials.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Polynomial control and sector data for Puiseux expansions.

  1. lemma OAI.DegeneratingTrees.Clock.sector_sqrt_le_re line 16
  2. lemma OAI.DegeneratingTrees.Clock.real_power_exp_sqrt line 38
  3. lemma OAI.DegeneratingTrees.Clock.polynomial_sector_slow line 55
  4. lemma OAI.DegeneratingTrees.Clock.sector_radial_eventually line 89
  5. lemma OAI.DegeneratingTrees.Clock.sector_halfplane_analytic line 94
  6. lemma OAI.DegeneratingTrees.Clock.sector_analytic_eq_of_ray line 101
  7. def OAI.DegeneratingTrees.Clock.PuiseuxSector line 112
  8. lemma OAI.DegeneratingTrees.Clock.PuiseuxSector.slow_and_dichotomy line 115
  9. lemma OAI.DegeneratingTrees.Clock.PuiseuxSector.inv_analytic line 133
  10. theorem OAI.DegeneratingTrees.Clock.puiseux_lowerSectorData line 143