OAI/Probability/Ballisticity/Estimates/RapidDecay.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.RapidDecay line 12
  2. lemma OAI.DirectionalTransience.RapidDecay.of_le line 15
  3. lemma OAI.DirectionalTransience.RapidDecay.add line 23
  4. lemma OAI.DirectionalTransience.RapidDecay.const_mul line 28
  5. lemma OAI.DirectionalTransience.RapidDecay.pow_mul line 33
  6. lemma OAI.DirectionalTransience.RapidDecay.shift line 38
  7. lemma OAI.DirectionalTransience.rapidDecay_of_power_bounds line 47
  8. lemma OAI.DirectionalTransience.rapidDecay_of_weighted_limit line 66
  9. lemma OAI.DirectionalTransience.power_stretchedExp_limit line 79
  10. lemma OAI.DirectionalTransience.rapidDecay_stretchedExp line 89
  11. lemma OAI.DirectionalTransience.rapidDecay_geometric line 97
  12. lemma OAI.DirectionalTransience.descending_probability_bound line 109