OAI/Probability/DirectionalWalk/WordPosterior.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalZeroOne.firstVisitIndex line 14
  2. lemma OAI.DirectionalZeroOne.firstVisitIndex_eq line 17
  3. lemma OAI.DirectionalZeroOne.firstVisitIndex_fiber line 20
  4. lemma OAI.DirectionalZeroOne.measurable_firstVisitIndex line 35
  5. def OAI.DirectionalZeroOne.firstVisitWord line 51
  6. lemma OAI.DirectionalZeroOne.measurable_firstVisitWord line 54
  7. lemma OAI.DirectionalZeroOne.firstVisitWord_spec line 58
  8. lemma OAI.DirectionalZeroOne.firstVisitWord_eq_of_cylinder line 71
  9. lemma OAI.DirectionalZeroOne.firstVisitWord_fiber_ae line 80
  10. lemma OAI.DirectionalZeroOne.firstVisitWord_map_eq line 97
  11. def OAI.DirectionalZeroOne.continuationLaw line 111
  12. lemma OAI.DirectionalZeroOne.continuationLaw_probability line 114
  13. lemma OAI.DirectionalZeroOne.annealed_disjoint_prefix_tail' line 119
  14. lemma OAI.DirectionalZeroOne.continuationLaw_fresh_cylinder line 133
  15. lemma OAI.DirectionalZeroOne.firstHitWords_full_of_cylinder_eq line 148
  16. lemma OAI.DirectionalZeroOne.continuationLaw_fresh_stopped line 168
  17. def OAI.DirectionalZeroOne.wordPosterior line 183
  18. def OAI.DirectionalZeroOne.endpointPosterior line 187
  19. lemma OAI.DirectionalZeroOne.wordCylinder_prefixWord line 191
  20. lemma OAI.DirectionalZeroOne.endpointPosterior_eq_ratio line 200
  21. lemma OAI.DirectionalZeroOne.measurable_prefixWord_filtration line 205
  22. lemma OAI.DirectionalZeroOne.endpointPosterior_adapted line 211
  23. lemma OAI.DirectionalZeroOne.endpointPosterior_condExp line 215
  24. lemma OAI.DirectionalZeroOne.endpointPosterior_martingale line 225
  25. lemma OAI.DirectionalZeroOne.wordPosterior_bounds line 232
  26. lemma OAI.DirectionalZeroOne.endpointPosterior_bounds line 248
  27. lemma OAI.DirectionalZeroOne.endpointPosterior_prefix line 256
  28. def OAI.DirectionalZeroOne.wordEndpointMax line 263
  29. lemma OAI.DirectionalZeroOne.wordEndpointMax_prefixWord line 267
  30. lemma OAI.DirectionalZeroOne.wordEndpointMax_bounds line 281
  31. lemma OAI.DirectionalZeroOne.stoppedEndpointMax_le line 288
  32. lemma OAI.DirectionalZeroOne.stoppedEndpointMax_exponential line 298
  33. lemma OAI.DirectionalZeroOne.stoppedEndpointMax_joint_weight line 323