OAI/Probability/Ballisticity/Estimates/OrderedTimes.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.gaussian_block_count_limit line 12
  2. lemma OAI.DirectionalTransience.tendstoInMeasure_sub_zero line 23
  3. lemma OAI.DirectionalTransience.fluctuationScale_nonneg line 43
  4. lemma OAI.DirectionalTransience.disjoint_blocks_injective line 48
  5. lemma OAI.DirectionalTransience.realPartialSum_sub_eq_block line 61
  6. theorem OAI.DirectionalTransience.gaussian_polygon_increment_limit line 69
  7. def OAI.DirectionalTransience.orderedTimes line 134
  8. lemma OAI.DirectionalTransience.orderedTimes_monotone line 137
  9. lemma OAI.DirectionalTransience.orderedTimes_succ line 145
  10. def OAI.DirectionalTransience.incrementCumsum line 148
  11. lemma OAI.DirectionalTransience.incrementCumsum_eval line 154
  12. def OAI.DirectionalTransience.gaussianPathFiniteLaw line 161
  13. instance OAI.DirectionalTransience.gaussianPathFiniteLaw_probability line 166
  14. lemma OAI.DirectionalTransience.ordered_adjacent_disjoint line 171
  15. theorem OAI.DirectionalTransience.gaussian_polygon_finite_limit line 178
  16. lemma OAI.DirectionalTransience.continuous_path_restrict line 207
  17. lemma OAI.DirectionalTransience.continuous_path_measure_ext line 213
  18. theorem OAI.DirectionalTransience.exists_path_limit_of_tight_finite_limit line 241
  19. theorem OAI.DirectionalTransience.gaussian_iid_path_limit line 282
  20. theorem OAI.DirectionalTransience.transverse_common_gaussian_path_limit line 327
  21. def OAI.DirectionalTransience.renewalSum line 358
  22. lemma OAI.DirectionalTransience.renewalSum_zero line 360
  23. lemma OAI.DirectionalTransience.renewalSum_succ line 361
  24. lemma OAI.DirectionalTransience.renewalSum_ge line 363
  25. lemma OAI.DirectionalTransience.renewalSum_strictMono line 367
  26. def OAI.DirectionalTransience.renewalCount line 374
  27. lemma OAI.DirectionalTransience.renewalCount_le line 376
  28. lemma OAI.DirectionalTransience.renewalCount_lower line 377
  29. lemma OAI.DirectionalTransience.renewalCount_upper line 381
  30. lemma OAI.DirectionalTransience.renewalCount_zero line 388
  31. lemma OAI.DirectionalTransience.renewalCount_monotone line 389
  32. lemma OAI.DirectionalTransience.linear_error_uniform line 393