OAI/Analysis/PathSelection/SectorLimits.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Sector filters, subexponential estimates and grouped leading coefficients.

  1. def OAI.DegeneratingTrees.sectorInfinity line 16
  2. lemma OAI.DegeneratingTrees.eventually_sectorInfinity line 22
  3. instance OAI.DegeneratingTrees.sectorInfinity_neBot line 25
  4. lemma OAI.DegeneratingTrees.tendsto_norm_sectorInfinity line 33
  5. lemma OAI.DegeneratingTrees.tendsto_real_sectorInfinity line 41
  6. lemma OAI.DegeneratingTrees.tendsto_re_sectorInfinity line 48
  7. def OAI.DegeneratingTrees.Clock.ExpBound line 84
  8. def OAI.DegeneratingTrees.Clock.ExpSmall line 87
  9. def OAI.DegeneratingTrees.Clock.SectorSlow line 89
  10. lemma OAI.DegeneratingTrees.Clock.ExpBound.mono line 91
  11. lemma OAI.DegeneratingTrees.Clock.ExpBound.mul line 99
  12. lemma OAI.DegeneratingTrees.Clock.ExpBound.add line 103
  13. lemma OAI.DegeneratingTrees.Clock.ExpSmall.mono line 106
  14. lemma OAI.DegeneratingTrees.Clock.ExpSmall.add line 111
  15. lemma OAI.DegeneratingTrees.Clock.ExpSmall.mul line 117
  16. def OAI.DegeneratingTrees.Subexponential line 135
  17. lemma OAI.DegeneratingTrees.log_div_tendsto_zero line 138
  18. lemma OAI.DegeneratingTrees.exponent_ratio_zero line 143
  19. theorem OAI.DegeneratingTrees.subexponential_of_lower_size_bound line 157
  20. theorem OAI.DegeneratingTrees.negative_exponential_times_subexponential line 173
  21. lemma OAI.DegeneratingTrees.Subexponential.const line 187
  22. lemma OAI.DegeneratingTrees.Subexponential.mul line 194
  23. theorem OAI.DegeneratingTrees.exists_first_coefficient line 219
  24. lemma OAI.DegeneratingTrees.normalized_grouped_error line 245
  25. theorem OAI.DegeneratingTrees.grouped_leading_normalization line 271
  26. theorem OAI.DegeneratingTrees.grouped_normalization_or_zero_coefficients line 293