OAI/Probability/Ballisticity/Geometry/WordHeightGain.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.renewal_occupation_lower line 12
  2. lemma OAI.DirectionalTransience.nat_integrable_of_truncated_mean_bound line 46
  3. lemma OAI.DirectionalTransience.renewal_mean_bound line 83
  4. lemma OAI.DirectionalTransience.trueRecord_eq_regenerationTime line 111
  5. lemma OAI.DirectionalTransience.conditioned_wordRecordCount_integrable line 134
  6. lemma OAI.DirectionalTransience.height_le_recordCount line 168
  7. lemma OAI.DirectionalTransience.wordPath_step_or_stay line 189
  8. lemma OAI.DirectionalTransience.dot_step line 199
  9. def OAI.DirectionalTransience.wordHeightGain line 208
  10. lemma OAI.DirectionalTransience.wordHeightGain_le_recordCount line 211
  11. lemma OAI.DirectionalTransience.wordHeightGain_positive line 225
  12. lemma OAI.DirectionalTransience.conditioned_wordHeightGain_moments line 230
  13. lemma OAI.DirectionalTransience.nonnegative_interval_count line 264
  14. lemma OAI.DirectionalTransience.stationary_initial_average_bound line 323
  15. lemma OAI.DirectionalTransience.integrable_min_nonneg line 391
  16. def OAI.DirectionalTransience.truncatedMean line 400
  17. lemma OAI.DirectionalTransience.truncatedMean_nonneg line 403
  18. lemma OAI.DirectionalTransience.truncatedMean_mono line 408
  19. lemma OAI.DirectionalTransience.truncatedMean_mul_le line 416