OAI/Probability/Ballisticity/Walk/UpperKernel.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DirectionalTransience.UpperRows line 12
  2. def OAI.DirectionalTransience.upperEnvironment line 14
  3. lemma OAI.DirectionalTransience.upperEnvironment_continuous line 17
  4. lemma OAI.DirectionalTransience.upperEnvironment_lift line 21
  5. lemma OAI.DirectionalTransience.continuous_wordWeight line 26
  6. lemma OAI.DirectionalTransience.hitKernel_eq_tsum_words line 34
  7. lemma OAI.DirectionalTransience.hitKernel_lowerSemicontinuous line 44
  8. def OAI.DirectionalTransience.upperHorizontalKernel line 51
  9. lemma OAI.DirectionalTransience.upperHorizontalKernel_apply line 56
  10. lemma OAI.DirectionalTransience.upperHorizontalKernel_lowerSemicontinuous line 65
  11. lemma OAI.DirectionalTransience.upperHorizontalKernel_mass_le_one line 72
  12. lemma OAI.DirectionalTransience.wordPath_endpoint_sum line 87
  13. lemma OAI.DirectionalTransience.wordPath_replicate_min line 93
  14. lemma OAI.DirectionalTransience.exists_horizontal_word line 104
  15. lemma OAI.DirectionalTransience.wordPath_horizontal line 151
  16. lemma OAI.DirectionalTransience.positive_wordWeight line 165
  17. lemma OAI.DirectionalTransience.upperHorizontalKernel_pos line 173