OAI/Probability/DirectionalWalk/LateContacts.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalZeroOne.lateContactEvent line 12
  2. lemma OAI.DirectionalZeroOne.lateContactEvent_bound line 21
  3. lemma OAI.DirectionalZeroOne.conditioned_bridge_late_bound line 43
  4. lemma OAI.DirectionalZeroOne.iid_tape_strongLaw line 65
  5. lemma OAI.DirectionalZeroOne.tapeHeight_strongLaw line 81
  6. lemma OAI.DirectionalZeroOne.firstCommonBlock_height line 88
  7. lemma OAI.DirectionalZeroOne.commonDepth_strongLaw line 94
  8. lemma OAI.DirectionalZeroOne.placed_slab_positive line 141
  9. lemma OAI.DirectionalZeroOne.placed_common_lower line 148
  10. lemma OAI.DirectionalZeroOne.placed_common_data line 164
  11. lemma OAI.DirectionalZeroOne.placed_slabRadius_integrable line 179
  12. lemma OAI.DirectionalZeroOne.placed_wordEnd_integrable line 192
  13. lemma OAI.DirectionalZeroOne.concatenateWords_end line 201
  14. lemma OAI.DirectionalZeroOne.concatenateList_end line 212
  15. lemma OAI.DirectionalZeroOne.fin_prefix_sum_castSucc line 215
  16. lemma OAI.DirectionalZeroOne.fin_prefix_sum_last line 223
  17. lemma OAI.DirectionalZeroOne.concatenateWords_site line 231
  18. lemma OAI.DirectionalZeroOne.fin_reverse_prefix_sum line 260
  19. lemma OAI.DirectionalZeroOne.fin_prefix_sum_range line 271
  20. lemma OAI.DirectionalZeroOne.reversePrefix_site line 283