OAI/Analysis/PathSelection/ClockComposition.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Weighted words and holomorphic finite-clock and Puiseux tuple composition.

  1. lemma OAI.DegeneratingTrees.Clock.weighted_truncation_words line 16
  2. def OAI.DegeneratingTrees.Clock.weightedCoefficient line 40
  3. lemma OAI.DegeneratingTrees.Clock.weighted_coefficient_truncation line 43
  4. lemma OAI.DegeneratingTrees.Clock.weighted_split line 75
  5. lemma OAI.DegeneratingTrees.Clock.weightedCoefficient_slow line 89
  6. lemma OAI.DegeneratingTrees.Clock.ExpSmall.analytic_comp_difference line 107
  7. lemma OAI.DegeneratingTrees.Clock.SectorSlow.of_tendsto line 115
  8. theorem OAI.DegeneratingTrees.Clock.SectorExpansion.holomorphic_comp_negative line 122
  9. lemma OAI.DegeneratingTrees.Clock.Puiseux.uniform line 197
  10. lemma OAI.DegeneratingTrees.Clock.SectorExpansion.uniform line 202
  11. lemma OAI.DegeneratingTrees.Clock.ClockGerm.uniform line 208
  12. lemma OAI.DegeneratingTrees.Clock.Puiseux.analytic_comp_finite line 216
  13. theorem OAI.DegeneratingTrees.Clock.ClockGerm.analytic_comp_finite line 240
  14. lemma OAI.DegeneratingTrees.Clock.Puiseux.finite_representation line 321
  15. lemma OAI.DegeneratingTrees.Clock.finite_representation_refine line 339
  16. lemma OAI.DegeneratingTrees.Clock.puiseux_tuple_finite_representation line 350
  17. theorem OAI.DegeneratingTrees.Clock.Puiseux.analytic_comp_tuple_finite line 392