OAI/Analysis/PathSelection/RelativeStrips.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Derivative growth, relative strips and inverse clock ratios.

  1. lemma OAI.DegeneratingTrees.Clock.real_log_derivative_bound line 15
  2. lemma OAI.DegeneratingTrees.Clock.complex_re_log_derivative line 40
  3. theorem OAI.DegeneratingTrees.Clock.complex_log_derivative_power_bound line 50
  4. lemma OAI.DegeneratingTrees.Clock.unbounded_log_exponent_order line 88
  5. lemma OAI.DegeneratingTrees.Clock.norm_sub_real_part line 128
  6. theorem OAI.DegeneratingTrees.Clock.relative_strip_estimate line 132
  7. lemma OAI.DegeneratingTrees.Clock.relative_strip_log_deriv_bound line 175
  8. lemma OAI.DegeneratingTrees.Clock.relative_strip_log_deriv_tendsto line 238
  9. lemma OAI.DegeneratingTrees.Clock.SectorSlow.relative_strip line 312
  10. theorem OAI.DegeneratingTrees.Clock.relative_strip_pair_estimate line 334
  11. lemma OAI.DegeneratingTrees.Clock.exponential_normalized_log_deriv line 387
  12. theorem OAI.DegeneratingTrees.Clock.affine_relative_strip_pair_estimate line 405
  13. lemma OAI.DegeneratingTrees.Clock.inverse_increment_error_tendsto line 441
  14. lemma OAI.DegeneratingTrees.Clock.inverse_pair_bounded line 454
  15. theorem OAI.DegeneratingTrees.Clock.inverse_clock_ratio_tendsto line 479
  16. lemma OAI.DegeneratingTrees.Clock.inverse_clock_modulus_tendsto line 521