OAI/Analysis/PathSelection/PuiseuxInverses.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Puiseux inverses, composition and sector bounds.

  1. lemma OAI.DegeneratingTrees.Clock.rootCoord_inverse_power line 15
  2. lemma OAI.DegeneratingTrees.Clock.rootCoord_monomial line 24
  3. lemma OAI.DegeneratingTrees.Clock.tail_right_inverse line 38
  4. lemma OAI.DegeneratingTrees.Clock.Puiseux.normalize_unbounded_real line 63
  5. lemma OAI.DegeneratingTrees.Clock.analytic_inverse_factor line 113
  6. theorem OAI.DegeneratingTrees.Clock.Puiseux.inverse_change line 138
  7. def OAI.DegeneratingTrees.Clock.radialInfinity line 198
  8. def OAI.DegeneratingTrees.Clock.complexRoot line 200
  9. lemma OAI.DegeneratingTrees.Clock.complexRoot_norm line 202
  10. lemma OAI.DegeneratingTrees.Clock.complexRoot_real line 205
  11. lemma OAI.DegeneratingTrees.Clock.complexRoot_tendsto_zero line 208
  12. lemma OAI.DegeneratingTrees.Clock.complexRoot_analytic line 214
  13. lemma OAI.DegeneratingTrees.Clock.complexRoot_zpow line 218
  14. lemma OAI.DegeneratingTrees.Clock.radial_eventually line 225
  15. theorem OAI.DegeneratingTrees.Clock.Puiseux.sector_leading line 232
  16. lemma OAI.DegeneratingTrees.Clock.rootCoord_scaled_power line 269
  17. theorem OAI.DegeneratingTrees.Clock.Puiseux.comp_unbounded line 281
  18. theorem OAI.DegeneratingTrees.Clock.Puiseux.change_coordinate line 348
  19. lemma OAI.DegeneratingTrees.Clock.radial_real_tendsto line 367
  20. lemma OAI.DegeneratingTrees.Clock.radial_norm_equivalent line 372
  21. theorem OAI.DegeneratingTrees.Clock.Puiseux.sector_modulus_comparable line 392