OAI/Probability/Ballisticity/Estimates/LowerClip.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.inverse_moment_of_geometric_tail line 12
  2. lemma OAI.DirectionalTransience.exists_positive_step line 54
  3. lemma OAI.DirectionalTransience.quenched_noDrop_positive_of_directionallyTransient line 68
  4. lemma OAI.DirectionalTransience.noDrop_inverse_moment line 76
  5. lemma OAI.DirectionalTransience.integer_quantile line 88
  6. lemma OAI.DirectionalTransience.order_mass_cut line 124
  7. def OAI.DirectionalTransience.lowerClip line 167
  8. lemma OAI.DirectionalTransience.lowerClip_tendsto line 169
  9. lemma OAI.DirectionalTransience.lowerClip_sub_bound line 178
  10. lemma OAI.DirectionalTransience.integral_le_zero_of_identDistrib_lower_bound line 197
  11. def OAI.DirectionalTransience.prefixMax line 245
  12. lemma OAI.DirectionalTransience.prefixMax_nonneg line 249
  13. lemma OAI.DirectionalTransience.prefixMax_le_truncation line 254
  14. lemma OAI.DirectionalTransience.integrable_prefixMax line 266
  15. lemma OAI.DirectionalTransience.integral_prefixMax_le line 274
  16. lemma OAI.DirectionalTransience.integral_prefixMax_div_tendsto_zero line 303
  17. lemma OAI.DirectionalTransience.le_prefixMax line 348
  18. lemma OAI.DirectionalTransience.log_sum_le_log_add_prefixMax line 356
  19. lemma OAI.DirectionalTransience.integral_log_sum_div_tendsto_zero line 375