OAI/Analysis/PathSelection/UniformFamilies.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Coefficient vanishing, uniform clock expansions and holomorphic family limits.

  1. theorem OAI.DegeneratingTrees.sector_common_zero_of_ray_zero line 18
  2. lemma OAI.DegeneratingTrees.Clock.SectorExpansion.positive_coeff_zero_of_limit line 60
  3. structure OAI.DegeneratingTrees.Clock.UniformSectorExpansion line 97
  4. lemma OAI.DegeneratingTrees.Clock.UniformSectorExpansion.eventually_analytic line 107
  5. lemma OAI.DegeneratingTrees.Clock.UniformSectorExpansion.scalarize line 113
  6. lemma OAI.DegeneratingTrees.Clock.uniform_sector_eq_of_ray line 130
  7. lemma OAI.DegeneratingTrees.Clock.UniformSectorExpansion.positive_coeff_zero line 147
  8. def OAI.DegeneratingTrees.Clock.zeroCoefficient line 163
  9. lemma OAI.DegeneratingTrees.Clock.UniformSectorExpansion.zero_cutoff_error line 169
  10. def OAI.DegeneratingTrees.Clock.UniformPuiseux line 221
  11. lemma OAI.DegeneratingTrees.Clock.UniformPuiseux.scalarize line 225
  12. lemma OAI.DegeneratingTrees.Clock.UniformPuiseux.normalize line 233
  13. lemma OAI.DegeneratingTrees.Clock.UniformPuiseux.finite_limit_nonnegative line 250
  14. lemma OAI.DegeneratingTrees.Clock.UniformPuiseux.finite_limit_representative line 272
  15. def OAI.DegeneratingTrees.Clock.UniformClockGerm line 317
  16. lemma OAI.DegeneratingTrees.Clock.UniformClockGerm.scalarize line 325
  17. lemma OAI.DegeneratingTrees.Clock.UniformPuiseux.first_clock_limit line 338
  18. lemma OAI.DegeneratingTrees.Clock.tendsto_of_comp_clock line 381
  19. lemma OAI.DegeneratingTrees.Clock.ValidClocks.previous_chart line 389
  20. lemma OAI.DegeneratingTrees.Clock.uniform_expansion_limit line 432
  21. theorem OAI.DegeneratingTrees.Clock.UniformClockGerm.model_limit line 473
  22. theorem OAI.DegeneratingTrees.Clock.UniformClockGerm.last_clock_limit line 502