OAI/Analysis/PathSelection/ClockExpansions.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Clock expansions, uniform bounds and convolution.

  1. structure OAI.DegeneratingTrees.Clock.SectorExpansion line 19
  2. lemma OAI.DegeneratingTrees.Clock.central_re_lower line 29
  3. lemma OAI.DegeneratingTrees.Clock.AdmissibleAngularLoss.central_tail line 39
  4. lemma OAI.DegeneratingTrees.Clock.SectorExpansion.empty line 51
  5. lemma OAI.DegeneratingTrees.Clock.exists_greatest_of_finite_above line 89
  6. theorem OAI.DegeneratingTrees.Clock.SectorExpansion.leading line 107
  7. theorem OAI.DegeneratingTrees.Clock.SectorExpansion.leading_or_zero line 141
  8. lemma OAI.DegeneratingTrees.Clock.ExpBound.zero line 165
  9. lemma OAI.DegeneratingTrees.Clock.ExpBound.neg line 166
  10. lemma OAI.DegeneratingTrees.Clock.ExpBound.sub line 168
  11. lemma OAI.DegeneratingTrees.Clock.ExpBound.sum line 171
  12. lemma OAI.DegeneratingTrees.Clock.ExpSmall.zero line 180
  13. lemma OAI.DegeneratingTrees.Clock.ExpSmall.neg line 181
  14. lemma OAI.DegeneratingTrees.Clock.ExpSmall.sub line 185
  15. lemma OAI.DegeneratingTrees.Clock.ExpSmall.sum line 188
  16. lemma OAI.DegeneratingTrees.Clock.ExpBound.cexp line 197
  17. lemma OAI.DegeneratingTrees.Clock.ExpBound.expTerm line 201
  18. lemma OAI.DegeneratingTrees.Clock.SectorSlow.mul line 204
  19. lemma OAI.DegeneratingTrees.Clock.SectorSlow.expSmall line 210
  20. lemma OAI.DegeneratingTrees.Clock.SectorExpansion.eventually_analytic line 214
  21. lemma OAI.DegeneratingTrees.Clock.SectorExpansion.expSmall_remainder line 219
  22. lemma OAI.DegeneratingTrees.Clock.SectorExpansion.of_expSmall line 226
  23. lemma OAI.DegeneratingTrees.Clock.SectorExpansion.expBound line 241
  24. lemma OAI.DegeneratingTrees.Clock.truncation_expBound line 255
  25. def OAI.DegeneratingTrees.Clock.exponentConvolution line 278
  26. lemma OAI.DegeneratingTrees.Clock.convolution_truncation line 281
  27. lemma OAI.DegeneratingTrees.Clock.product_truncation_rectangle line 314
  28. lemma OAI.DegeneratingTrees.Clock.rectangle_high line 329
  29. lemma OAI.DegeneratingTrees.Clock.rectangle_split line 343