OAI/Analysis/PathSelection/RealClocks.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Real leading terms, conjugation and logarithmic derivative bounds.

  1. lemma OAI.DegeneratingTrees.Clock.SectorExpansion.top_nonnegative line 15
  2. theorem OAI.DegeneratingTrees.Clock.ExpansionOver.puiseux_unbounded_leading line 28
  3. lemma OAI.DegeneratingTrees.Clock.analyticAt_reflection line 80
  4. lemma OAI.DegeneratingTrees.Clock.mem_lossSector_star line 87
  5. lemma OAI.DegeneratingTrees.Clock.SectorExpansion.conj line 96
  6. lemma OAI.DegeneratingTrees.Clock.ClockGerm.conj line 110
  7. lemma OAI.DegeneratingTrees.Clock.SectorExpansion.congr_coeff line 136
  8. lemma OAI.DegeneratingTrees.Clock.SectorExpansion.add_same line 149
  9. lemma OAI.DegeneratingTrees.Clock.PuiseuxSector.reflect line 159
  10. lemma OAI.DegeneratingTrees.Clock.ExpansionOver.puiseux_real_expansion line 166
  11. lemma OAI.DegeneratingTrees.Clock.positive_real_factor_of_normalized line 189
  12. theorem OAI.DegeneratingTrees.Clock.ExpansionOver.puiseux_positive_leading line 208
  13. lemma OAI.DegeneratingTrees.Clock.log_deriv_bound_of_log_norm_bound line 253
  14. lemma OAI.DegeneratingTrees.Clock.SectorSlow.log_deriv_tendsto line 319
  15. lemma OAI.DegeneratingTrees.Clock.LowerSectorData.log_deriv_strip line 401
  16. lemma OAI.DegeneratingTrees.Clock.SectorExpansion.log_deriv_strip line 406
  17. lemma OAI.DegeneratingTrees.Clock.ExpansionOver.real_expansion line 436
  18. theorem OAI.DegeneratingTrees.Clock.ExpansionOver.positive_leading_strip line 460