OAI/Probability/Ballisticity/Geometry/WordCoordinate.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.ratio_hit_geometric line 12
  2. lemma OAI.DirectionalTransience.forwardTemplate_probability_lower line 35
  3. lemma OAI.DirectionalTransience.ratio_hit_union_bound line 53
  4. lemma OAI.DirectionalTransience.annealed_ge_noDrop_mul_conditioned line 70
  5. lemma OAI.DirectionalTransience.large_excursion_ratio line 83
  6. lemma OAI.DirectionalTransience.conditioned_polynomial_ratio_lower line 111
  7. lemma OAI.DirectionalTransience.firstWord_height_nonneg line 156
  8. lemma OAI.DirectionalTransience.geometric_beats_affine line 164
  9. lemma OAI.DirectionalTransience.nonintegrable_radius_scale line 176
  10. lemma OAI.DirectionalTransience.radius_integrable_of_template_constants line 213
  11. lemma OAI.DirectionalTransience.unit_direction_coordinate_bound line 323
  12. lemma OAI.DirectionalTransience.conditioned_wordRadius_integrable line 332
  13. lemma OAI.DirectionalTransience.increment_sublinear_of_average line 378
  14. def OAI.DirectionalTransience.wordCoordinate line 394
  15. lemma OAI.DirectionalTransience.wordCoordinate_abs_le_radius line 397
  16. lemma OAI.DirectionalTransience.conditioned_wordCoordinate_integrable line 401
  17. lemma OAI.DirectionalTransience.conditioned_coordinate_positive_mean line 410