OAI/Analysis/PathSelection/ExponentSupports.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Locally finite real exponent supports, finite convolution and negative words.

  1. def OAI.DegeneratingTrees.Clock.exponentSum line 14
  2. def OAI.DegeneratingTrees.Clock.exponentPairs line 15
  3. def OAI.DegeneratingTrees.Clock.exponentFiber line 17
  4. lemma OAI.DegeneratingTrees.Clock.exponentPairs_finite line 20
  5. lemma OAI.DegeneratingTrees.Clock.exponentFiber_finite line 30
  6. lemma OAI.DegeneratingTrees.Clock.exponentSum_bddAbove line 35
  7. lemma OAI.DegeneratingTrees.Clock.exponentSum_finite line 43
  8. lemma OAI.DegeneratingTrees.Clock.exponentPairs_subset_rectangle line 52
  9. def OAI.DegeneratingTrees.Clock.prependPair line 71
  10. lemma OAI.DegeneratingTrees.Clock.prependPair_injective line 72
  11. def OAI.DegeneratingTrees.Clock.wordsOfLength line 76
  12. lemma OAI.DegeneratingTrees.Clock.mem_wordsOfLength line 80
  13. def OAI.DegeneratingTrees.Clock.wordsUpTo line 104
  14. lemma OAI.DegeneratingTrees.Clock.mem_wordsUpTo line 107
  15. def OAI.DegeneratingTrees.Clock.exponentWords line 116
  16. def OAI.DegeneratingTrees.Clock.wordCut line 117
  17. def OAI.DegeneratingTrees.Clock.wordFiber line 118
  18. def OAI.DegeneratingTrees.Clock.wordSupport line 119
  19. lemma OAI.DegeneratingTrees.Clock.list_sum_le_length line 121
  20. lemma OAI.DegeneratingTrees.Clock.list_sum_le_member line 131
  21. lemma OAI.DegeneratingTrees.Clock.wordCut_subset_words line 146
  22. lemma OAI.DegeneratingTrees.Clock.wordCut_finite line 162
  23. lemma OAI.DegeneratingTrees.Clock.wordFiber_finite line 172
  24. lemma OAI.DegeneratingTrees.Clock.wordSupport_bddAbove line 177
  25. lemma OAI.DegeneratingTrees.Clock.wordSupport_finite line 183