OAI/Analysis/PathSelection/PuiseuxCalculus.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Puiseux expansions, differentiation and analytic Hardy properties.

  1. def OAI.DegeneratingTrees.Clock.rootCoord line 14
  2. def OAI.DegeneratingTrees.Clock.Puiseux line 16
  3. lemma OAI.DegeneratingTrees.Clock.rootCoord_pos line 20
  4. lemma OAI.DegeneratingTrees.Clock.rootCoord_tendsto_zero line 23
  5. lemma OAI.DegeneratingTrees.Clock.rootCoord_complex_tendsto_zero line 27
  6. lemma OAI.DegeneratingTrees.Clock.rootCoord_pow line 31
  7. lemma OAI.DegeneratingTrees.Clock.rootCoord_zpow line 38
  8. lemma OAI.DegeneratingTrees.Clock.Puiseux.congr line 44
  9. lemma OAI.DegeneratingTrees.Clock.puiseux_const line 48
  10. lemma OAI.DegeneratingTrees.Clock.Puiseux.normalize line 52
  11. lemma OAI.DegeneratingTrees.Clock.Puiseux.leading line 73
  12. lemma OAI.DegeneratingTrees.Clock.Puiseux.eventually_nonzero line 88
  13. lemma OAI.DegeneratingTrees.Clock.Puiseux.eventually_sign line 95
  14. lemma OAI.DegeneratingTrees.Clock.puiseux_refine line 131
  15. lemma OAI.DegeneratingTrees.Clock.Puiseux.mul line 147
  16. lemma OAI.DegeneratingTrees.Clock.Puiseux.neg line 161
  17. lemma OAI.DegeneratingTrees.Clock.Puiseux.add line 167
  18. lemma OAI.DegeneratingTrees.Clock.Puiseux.sub line 198
  19. lemma OAI.DegeneratingTrees.Clock.Puiseux.inv line 202
  20. lemma OAI.DegeneratingTrees.Clock.Puiseux.div line 211
  21. lemma OAI.DegeneratingTrees.Clock.analyticAt_conj_conj line 224
  22. lemma OAI.DegeneratingTrees.Clock.Puiseux.conj line 232
  23. lemma OAI.DegeneratingTrees.Clock.puiseux_analytic_root line 238
  24. lemma OAI.DegeneratingTrees.Clock.puiseux_ratPower line 243
  25. lemma OAI.DegeneratingTrees.Clock.eventuallyEq_deriv_atTop line 250
  26. lemma OAI.DegeneratingTrees.Clock.Puiseux.deriv line 258
  27. lemma OAI.DegeneratingTrees.Clock.analyticAt_real_rpow line 298
  28. lemma OAI.DegeneratingTrees.Clock.Puiseux.eventually_analytic line 304
  29. lemma OAI.DegeneratingTrees.Clock.Puiseux.real_eventually_analytic line 322
  30. lemma OAI.DegeneratingTrees.Clock.Puiseux.real_deriv line 327
  31. theorem OAI.DegeneratingTrees.Clock.Puiseux.eventually_monotone line 335