OAI/Analysis/PathSelection/ClockInverses.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Clock inversion, logarithmic strips and exponential inverse charts.

  1. lemma OAI.DegeneratingTrees.Clock.approximates_identity_of_deriv line 16
  2. theorem OAI.DegeneratingTrees.Clock.analytic_near_identity_inverse line 36
  3. def OAI.DegeneratingTrees.Clock.horizontalTail line 83
  4. lemma OAI.DegeneratingTrees.Clock.horizontalTail_open line 85
  5. lemma OAI.DegeneratingTrees.Clock.horizontalTail_convex line 89
  6. lemma OAI.DegeneratingTrees.Clock.closedBall_real_subset_horizontalTail line 94
  7. theorem OAI.DegeneratingTrees.Clock.analytic_inverse_on_tail_strip line 105
  8. def OAI.DegeneratingTrees.Clock.stripInfinity line 170
  9. lemma OAI.DegeneratingTrees.Clock.eventually_stripInfinity line 180
  10. instance OAI.DegeneratingTrees.Clock.stripInfinity_neBot line 183
  11. lemma OAI.DegeneratingTrees.Clock.stripInfinity_le_sectorInfinity line 190
  12. lemma OAI.DegeneratingTrees.Clock.tendsto_real_stripInfinity line 204
  13. lemma OAI.DegeneratingTrees.Clock.tendsto_re_stripInfinity line 211
  14. lemma OAI.DegeneratingTrees.Clock.SectorExpansion.log_deriv_tendsto line 227
  15. theorem OAI.DegeneratingTrees.Clock.ExpansionOver.puiseux_log_deriv line 258
  16. lemma OAI.DegeneratingTrees.Clock.analytic_log_on_convex line 293
  17. lemma OAI.DegeneratingTrees.Clock.analytic_ray_deriv_im_zero line 311
  18. theorem OAI.DegeneratingTrees.Clock.analytic_real_log_on_strip line 323
  19. theorem OAI.DegeneratingTrees.Clock.normalized_log_inverse line 389
  20. theorem OAI.DegeneratingTrees.Clock.positive_exponential_inverse line 443