OAI/Analysis/PathSelection/ClockDerivatives.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Differentiation and logarithmic derivatives of first clocks and Puiseux series.

  1. lemma OAI.DegeneratingTrees.Clock.hasDerivAt_expTerm line 15
  2. lemma OAI.DegeneratingTrees.Clock.analyticAt_expTerm line 23
  3. theorem OAI.DegeneratingTrees.Clock.SectorExpansion.deriv line 29
  4. lemma OAI.DegeneratingTrees.Clock.PuiseuxSector.deriv_mem line 80
  5. lemma OAI.DegeneratingTrees.Clock.ExpansionOver.puiseux_deriv line 87
  6. lemma OAI.DegeneratingTrees.Clock.Puiseux.sector_representative line 97
  7. lemma OAI.DegeneratingTrees.Clock.ClockGerm.first_of_lower line 104
  8. lemma OAI.DegeneratingTrees.Clock.ClockGerm.first_deriv line 116
  9. lemma OAI.DegeneratingTrees.Clock.Puiseux.log_deriv_tendsto line 146
  10. lemma OAI.DegeneratingTrees.Clock.PuiseuxSector.tendsto_of_ray line 186
  11. lemma OAI.DegeneratingTrees.Clock.PuiseuxSector.log_deriv_tendsto line 206