OAI/Probability/Ballisticity/Estimates/CellRadiusComparison.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.cell_radius_comparison line 12
  2. def OAI.DirectionalTransience.stageCellStarts line 52
  3. def OAI.DirectionalTransience.stageCellWidths line 54
  4. def OAI.DirectionalTransience.stageCellGaps line 56
  5. lemma OAI.DirectionalTransience.stage_cells_geometry line 59
  6. lemma OAI.DirectionalTransience.stage_cells_gap_bounds line 102
  7. lemma OAI.DirectionalTransience.eventually_exp_affine_le line 123
  8. lemma OAI.DirectionalTransience.eventually_mul_exp_le line 132
  9. lemma OAI.DirectionalTransience.eventually_stage_short_bound line 142
  10. lemma OAI.DirectionalTransience.cell_count_exp_bound line 166
  11. lemma OAI.DirectionalTransience.eventually_stage_probability_sum line 188