OAI/Analysis/PathSelection/ExponentialCharts.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Exponential sector charts, phase contraction and inward equal-exponent maps.

  1. theorem OAI.DegeneratingTrees.Clock.strict_exponential_chart line 17
  2. theorem OAI.DegeneratingTrees.Clock.inverse_halfplane_strip line 125
  3. lemma OAI.DegeneratingTrees.Clock.exp_horizontalTail_right line 163
  4. lemma OAI.DegeneratingTrees.Clock.exp_horizontalTail_norm line 168
  5. lemma OAI.DegeneratingTrees.Clock.imaginary_derivative_of_complex line 184
  6. lemma OAI.DegeneratingTrees.Clock.vertical_phase_derivative line 190
  7. theorem OAI.DegeneratingTrees.Clock.vertical_phase_contraction line 203
  8. lemma OAI.DegeneratingTrees.Clock.positive_quotient_neighborhood line 243
  9. theorem OAI.DegeneratingTrees.Clock.negative_log_quotient_on_strip line 264
  10. lemma OAI.DegeneratingTrees.Clock.arg_exp_eq_im_of_abs_lt_pi line 324
  11. theorem OAI.DegeneratingTrees.Clock.log_clock_phase_contraction line 334
  12. lemma OAI.DegeneratingTrees.Clock.log_inverse_ratio_derivative line 363
  13. theorem OAI.DegeneratingTrees.Clock.equal_exponent_inward line 394