OAI/Analysis/PathSelection/ClockAlgebra.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Multiplication, word polynomials, exponential decay and geometric inverses.

  1. theorem OAI.DegeneratingTrees.Clock.SectorExpansion.mul line 15
  2. lemma OAI.DegeneratingTrees.Clock.SectorSlow.sum line 64
  3. lemma OAI.DegeneratingTrees.Clock.convolution_slow line 69
  4. lemma OAI.DegeneratingTrees.Clock.convolution_analytic line 78
  5. def OAI.DegeneratingTrees.Clock.wordCoefficient line 103
  6. def OAI.DegeneratingTrees.Clock.wordTerm line 106
  7. lemma OAI.DegeneratingTrees.Clock.wordTerm_nil line 109
  8. lemma OAI.DegeneratingTrees.Clock.wordTerm_cons line 112
  9. lemma OAI.DegeneratingTrees.Clock.power_truncation_words line 118
  10. lemma OAI.DegeneratingTrees.Clock.geometric_truncation_words line 147
  11. def OAI.DegeneratingTrees.Clock.geometricCoefficient line 162
  12. lemma OAI.DegeneratingTrees.Clock.geometric_coefficient_truncation line 165
  13. lemma OAI.DegeneratingTrees.Clock.words_high line 195
  14. lemma OAI.DegeneratingTrees.Clock.geometric_split line 207
  15. lemma OAI.DegeneratingTrees.Clock.wordCoefficient_slow line 220
  16. lemma OAI.DegeneratingTrees.Clock.geometricCoefficient_slow line 234
  17. lemma OAI.DegeneratingTrees.Clock.ExpBound.const line 252
  18. lemma OAI.DegeneratingTrees.Clock.ExpBound.of_tendsto line 256
  19. lemma OAI.DegeneratingTrees.Clock.ExpBound.pow line 260
  20. lemma OAI.DegeneratingTrees.Clock.ExpBound.congr line 269
  21. lemma OAI.DegeneratingTrees.Clock.ExpSmall.congr line 272
  22. lemma OAI.DegeneratingTrees.Clock.ExpBound.tendsto_zero line 277
  23. lemma OAI.DegeneratingTrees.Clock.inverse_one_sub_tendsto line 283
  24. lemma OAI.DegeneratingTrees.Clock.inverse_one_sub_bound line 287
  25. lemma OAI.DegeneratingTrees.Clock.one_sub_eventually_ne line 290
  26. lemma OAI.DegeneratingTrees.Clock.inverse_difference_small line 296
  27. lemma OAI.DegeneratingTrees.Clock.geom_inverse_error line 307
  28. lemma OAI.DegeneratingTrees.Clock.SectorExpansion.negative_bound line 320
  29. lemma OAI.DegeneratingTrees.Clock.truncation_negative_bound line 335
  30. theorem OAI.DegeneratingTrees.Clock.SectorExpansion.geometric_inverse line 355
  31. lemma OAI.DegeneratingTrees.Clock.wordCoefficient_analytic line 398
  32. lemma OAI.DegeneratingTrees.Clock.geometricCoefficient_analytic line 413