OAI/Probability/Ballisticity/Estimates/WordDepartures.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.fresh_rows_factor line 12
  2. def OAI.DirectionalTransience.wordDepartures line 27
  3. def OAI.DirectionalTransience.wordWeight line 31
  4. lemma OAI.DirectionalTransience.wordWeight_nonneg line 36
  5. lemma OAI.DirectionalTransience.wordWeight_le_one line 42
  6. lemma OAI.DirectionalTransience.measurable_wordWeight_on line 50
  7. lemma OAI.DirectionalTransience.measurable_wordWeight line 63
  8. lemma OAI.DirectionalTransience.integrable_wordWeight line 68
  9. lemma OAI.DirectionalTransience.wordWeight_fresh_factor line 76
  10. def OAI.DirectionalTransience.wordPath line 84
  11. lemma OAI.DirectionalTransience.wordPath_zero line 89
  12. def OAI.DirectionalTransience.wordCylinder line 92
  13. lemma OAI.DirectionalTransience.measurableSet_wordCylinder line 95
  14. lemma OAI.DirectionalTransience.wordPath_transition_product line 102
  15. lemma OAI.DirectionalTransience.quenched_wordCylinder line 115
  16. lemma OAI.DirectionalTransience.annealed_wordCylinder line 133
  17. def OAI.DirectionalTransience.pathCylinder line 141
  18. lemma OAI.DirectionalTransience.measurableSet_pathCylinder line 144
  19. lemma OAI.DirectionalTransience.pathMeasure_ext line 151
  20. def OAI.DirectionalTransience.edgeWeight line 183
  21. lemma OAI.DirectionalTransience.transition_singleton line 186
  22. lemma OAI.DirectionalTransience.quenched_pathCylinder line 198
  23. lemma OAI.DirectionalTransience.quenched_pathCylinder_zero line 217
  24. lemma OAI.DirectionalTransience.edgeWeight_translation line 227
  25. lemma OAI.DirectionalTransience.quenched_translation line 236
  26. def OAI.DirectionalTransience.splicePath line 254
  27. lemma OAI.DirectionalTransience.splicePath_left line 257
  28. lemma OAI.DirectionalTransience.splicePath_right line 263
  29. lemma OAI.DirectionalTransience.pathCylinder_splice line 267
  30. lemma OAI.DirectionalTransience.splicePath_weight line 288
  31. lemma OAI.DirectionalTransience.quenched_prefix_markov line 304
  32. lemma OAI.DirectionalTransience.quenched_prefix_future line 330
  33. def OAI.DirectionalTransience.NoDrop line 340
  34. lemma OAI.DirectionalTransience.measurableSet_noDrop line 343
  35. lemma OAI.DirectionalTransience.dot_realPosition_add line 352
  36. lemma OAI.DirectionalTransience.dot_realPosition_sub line 356
  37. lemma OAI.DirectionalTransience.noDrop_translation line 360
  38. def OAI.DirectionalTransience.noDropQuenched line 369
  39. lemma OAI.DirectionalTransience.measurable_noDropQuenched line 372
  40. lemma OAI.DirectionalTransience.noDropQuenched_translation line 377
  41. lemma OAI.DirectionalTransience.annealed_noDrop_translation line 384
  42. def OAI.DirectionalTransience.FutureNoDrop line 392
  43. lemma OAI.DirectionalTransience.measurableSet_futureNoDrop line 395
  44. lemma OAI.DirectionalTransience.tendsto_atTop_has_minimum line 406
  45. def OAI.DirectionalTransience.extendPrefix line 416
  46. lemma OAI.DirectionalTransience.extendPrefix_apply line 419