OAI/Probability/Ballisticity/Geometry/HeightIncrement.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.block_transfer_bound line 18
  2. lemma OAI.DirectionalTransience.blockDecoration_finite_union line 46
  3. lemma OAI.DirectionalTransience.blockDecoration_small line 51
  4. lemma OAI.DirectionalTransience.renewal_height_block_subset line 72
  5. lemma OAI.DirectionalTransience.gaussian_renewal_block_modulus line 134
  6. theorem OAI.DirectionalTransience.heightGap_small_of_transfer line 171
  7. theorem OAI.DirectionalTransience.transverse_firstHit_uniform_error line 219
  8. def OAI.DirectionalTransience.heightIncrement line 265
  9. lemma OAI.DirectionalTransience.realPartialSum_heightIncrement line 267
  10. lemma OAI.DirectionalTransience.measurable_heightIncrement line 273
  11. lemma OAI.DirectionalTransience.height_polygon_difference_le line 277
  12. lemma OAI.DirectionalTransience.height_polygon_difference_small line 306
  13. lemma OAI.DirectionalTransience.commonBoundary_heightIncrement line 330
  14. theorem OAI.DirectionalTransience.transverse_firstHit_path_error line 335
  15. theorem OAI.DirectionalTransience.transverse_firstHit_path_limit line 368