OAI/Probability/DirectionalWalk/Slabs.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalZeroOne.conditioned line 10
  2. lemma OAI.DirectionalZeroOne.conditioned_probability line 13
  3. lemma OAI.DirectionalZeroOne.ae_conditioned_firstWord line 17
  4. lemma OAI.DirectionalZeroOne.conditioned_firstWord_suffix line 37
  5. lemma OAI.DirectionalZeroOne.measure_eq_tsum_fibres line 55
  6. def OAI.DirectionalZeroOne.slabLaw line 69
  7. lemma OAI.DirectionalZeroOne.slabLaw_probability line 72
  8. lemma OAI.DirectionalZeroOne.slabLaw_atom line 78
  9. lemma OAI.DirectionalZeroOne.ae_slabLaw_regeneration line 88
  10. lemma OAI.DirectionalZeroOne.firstWord_suffix_factorization line 96
  11. lemma OAI.DirectionalZeroOne.cutSuffix_measurePreserving line 114
  12. def OAI.DirectionalZeroOne.slabs line 133
  13. lemma OAI.DirectionalZeroOne.measurable_slabs line 136
  14. lemma OAI.DirectionalZeroOne.slabs_prefix_mass line 139
  15. lemma OAI.DirectionalZeroOne.slabs_map_eq_infinitePi line 169
  16. lemma OAI.DirectionalZeroOne.slabs_marginal line 205
  17. lemma OAI.DirectionalZeroOne.slabs_iid line 214