OAI/Probability/Ballisticity/Estimates/CurvePrefix.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.CurvePrefixAt line 14
  2. lemma OAI.DirectionalTransience.measurableSet_curvePrefixAt line 21
  3. lemma OAI.DirectionalTransience.curvePrefixAt_prefix line 36
  4. def OAI.DirectionalTransience.CurvePrefix line 50
  5. lemma OAI.DirectionalTransience.measurableSet_curvePrefix line 53
  6. lemma OAI.DirectionalTransience.curvePrefixAt_disjoint line 57
  7. lemma OAI.DirectionalTransience.quenched_curvePrefix_congr line 64
  8. lemma OAI.DirectionalTransience.measurable_quenched_curvePrefix_rows line 74
  9. def OAI.DirectionalTransience.curveEndpoint line 85
  10. lemma OAI.DirectionalTransience.curveEndpoint_apply line 89
  11. lemma OAI.DirectionalTransience.curveEndpoint_total line 98
  12. instance OAI.DirectionalTransience.curveEndpoint_finite line 105
  13. lemma OAI.DirectionalTransience.curveEndpoint_rows line 109
  14. lemma OAI.DirectionalTransience.curveEndpoint_future line 135
  15. def OAI.DirectionalTransience.curveWordEvent line 148
  16. lemma OAI.DirectionalTransience.measurableSet_curveWordEvent line 154
  17. lemma OAI.DirectionalTransience.curveWordEvent_cons_mass line 164