OAI/Analysis/PathSelection/ExpansionAlgebra.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Algebraic operations, shifts and leading terms of clock expansions.

  1. lemma OAI.DegeneratingTrees.Clock.SectorExpansion.const line 16
  2. lemma OAI.DegeneratingTrees.Clock.SectorExpansion.neg line 38
  3. lemma OAI.DegeneratingTrees.Clock.sum_indicator line 48
  4. lemma OAI.DegeneratingTrees.Clock.SectorExpansion.add line 68
  5. lemma OAI.DegeneratingTrees.Clock.ExpSmall.mul_slow line 119
  6. lemma OAI.DegeneratingTrees.Clock.SectorExpansion.mul_lower line 124
  7. def OAI.DegeneratingTrees.Clock.translatedSupport line 139
  8. lemma OAI.DegeneratingTrees.Clock.translatedSupport_bddAbove line 141
  9. lemma OAI.DegeneratingTrees.Clock.translatedSupport_finite line 149
  10. lemma OAI.DegeneratingTrees.Clock.translated_truncation line 156
  11. lemma OAI.DegeneratingTrees.Clock.SectorExpansion.exp_shift line 182
  12. lemma OAI.DegeneratingTrees.Clock.SectorExpansion.single line 198
  13. lemma OAI.DegeneratingTrees.Clock.SectorExpansion.erase line 231
  14. lemma OAI.DegeneratingTrees.Clock.strict_negative_support_gap line 265
  15. def OAI.DegeneratingTrees.Clock.nonzeroRaySupport line 285
  16. lemma OAI.DegeneratingTrees.Clock.SectorExpansion.trim_zero line 288
  17. theorem OAI.DegeneratingTrees.Clock.SectorExpansion.leading_or_zero_general line 331
  18. lemma OAI.DegeneratingTrees.Clock.SectorExpansion.leading_error line 361
  19. lemma OAI.DegeneratingTrees.Clock.ExpSmall.tendsto_zero line 371
  20. lemma OAI.DegeneratingTrees.Clock.SectorExpansion.uniform_leading line 377
  21. lemma OAI.DegeneratingTrees.Clock.SectorExpansion.uniform_leading_tendsto line 396
  22. lemma OAI.DegeneratingTrees.Clock.SectorExpansion.eventually_ne_of_leading line 403