OAI/Analysis/PathSelection/FilteredExpansions.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Filtered clock series, bounded expansions and finite decompositions.

  1. lemma OAI.DegeneratingTrees.Clock.negative_degree_cutoff line 16
  2. lemma OAI.DegeneratingTrees.Clock.negative_union_finite line 27
  3. lemma OAI.DegeneratingTrees.Clock.negative_fiber_finite line 40
  4. def OAI.DegeneratingTrees.Clock.degreeCoefficient line 54
  5. lemma OAI.DegeneratingTrees.Clock.degreeCoefficient_cutoff line 57
  6. lemma OAI.DegeneratingTrees.Clock.degree_truncation line 80
  7. theorem OAI.DegeneratingTrees.Clock.SectorExpansion.of_negative_degree_series line 124
  8. def OAI.DegeneratingTrees.Clock.BoundedExpansionOver line 160
  9. lemma OAI.DegeneratingTrees.Clock.BoundedExpansionOver.lower line 168
  10. lemma OAI.DegeneratingTrees.Clock.BoundedExpansionOver.zero line 174
  11. lemma OAI.DegeneratingTrees.Clock.BoundedExpansionOver.add line 181
  12. lemma OAI.DegeneratingTrees.Clock.BoundedExpansionOver.mul line 200
  13. lemma OAI.DegeneratingTrees.Clock.BoundedExpansionOver.sum line 212
  14. lemma OAI.DegeneratingTrees.Clock.BoundedExpansionOver.prod line 222
  15. lemma OAI.DegeneratingTrees.Clock.BoundedExpansionOver.negative_series line 232
  16. lemma OAI.DegeneratingTrees.Clock.filtered_positive_coeff_zero line 257
  17. lemma OAI.DegeneratingTrees.Clock.filtered_first_clock_limit line 280
  18. lemma OAI.DegeneratingTrees.Clock.filtered_previous_chart line 364
  19. lemma OAI.DegeneratingTrees.Clock.filtered_finite_decomposition line 396
  20. lemma OAI.DegeneratingTrees.Clock.filtered_model_limit line 442
  21. lemma OAI.DegeneratingTrees.Clock.ClockSectorData.finite_decomposition line 489
  22. lemma OAI.DegeneratingTrees.Clock.finite_common_positive line 502
  23. lemma OAI.DegeneratingTrees.Clock.BoundedExpansionOver.mono line 519