OAI/Analysis/PathSelection/SectorFamilies.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Countable sector narrowing and common fixed-sector asymptotics.

  1. lemma OAI.DegeneratingTrees.summable_common_eventual_majorant line 18
  2. theorem OAI.DegeneratingTrees.admissible_countable_majorant line 58
  3. theorem OAI.DegeneratingTrees.SectorEventually.countable line 84
  4. lemma OAI.DegeneratingTrees.fixed_sector_of_tendsto line 112
  5. lemma OAI.DegeneratingTrees.fixed_sector_of_littleO line 125
  6. lemma OAI.DegeneratingTrees.fixed_sector_realpart line 138