OAI/Probability/Ballisticity/Estimates/CommonWidthProcess.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.renewalCount_uniform line 12
  2. lemma OAI.DirectionalTransience.measurable_renewalCount line 39
  3. lemma OAI.DirectionalTransience.measure_tendsto_zero_of_ae_eventually_notMem line 47
  4. lemma OAI.DirectionalTransience.renewalCount_uniform_in_probability line 66
  5. def OAI.DirectionalTransience.commonWidthProcess line 89
  6. lemma OAI.DirectionalTransience.measurable_commonWidthProcess line 92
  7. def OAI.DirectionalTransience.commonMeanWidth line 97
  8. lemma OAI.DirectionalTransience.commonMeanWidth_ge_one line 100
  9. lemma OAI.DirectionalTransience.commonWidth_strongLaw line 113
  10. theorem OAI.DirectionalTransience.common_boundary_count_uniform line 128
  11. def OAI.DirectionalTransience.renewalRewardIncrement line 146
  12. lemma OAI.DirectionalTransience.renewalReward_sum line 149
  13. lemma OAI.DirectionalTransience.measurable_nat_select line 155
  14. lemma OAI.DirectionalTransience.measurable_renewalRewardIncrement line 160
  15. lemma OAI.DirectionalTransience.abs_convex_sub_le line 168
  16. lemma OAI.DirectionalTransience.renewalRewardPolygon_close line 179
  17. lemma OAI.DirectionalTransience.gaussian_renewal_path_error line 267
  18. theorem OAI.DirectionalTransience.gaussian_renewal_path_limit line 325
  19. theorem OAI.DirectionalTransience.transverse_common_boundary_path_limit line 351