OAI/Probability/DirectionalWalk/AxisCubes.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DirectionalZeroOne.CubeSite line 12
  2. abbrev OAI.DirectionalZeroOne.AxisCubeSite line 14
  3. lemma OAI.DirectionalZeroOne.card_cubeSite line 17
  4. lemma OAI.DirectionalZeroOne.card_axisCubeSite_le line 23
  5. lemma OAI.DirectionalZeroOne.axisCubeSite_nonempty line 28
  6. def OAI.DirectionalZeroOne.axisCubeEnumeration line 41
  7. lemma OAI.DirectionalZeroOne.axisCubeEnumeration_injective line 45
  8. lemma OAI.DirectionalZeroOne.axisCubeEnumeration_height line 53
  9. lemma OAI.DirectionalZeroOne.axisCubeEnumeration_surjective line 58
  10. lemma OAI.DirectionalZeroOne.abs_wordEnd_coord_le_radius line 67
  11. lemma OAI.DirectionalZeroOne.reversePrefix_endpoint_coord line 75
  12. lemma OAI.DirectionalZeroOne.cutIndex_le_height line 90
  13. lemma OAI.DirectionalZeroOne.reversed_cut_endpoint_radius line 97
  14. lemma OAI.DirectionalZeroOne.commonDepth_add line 110
  15. lemma OAI.DirectionalZeroOne.commonDepth_strictMono line 119
  16. lemma OAI.DirectionalZeroOne.common_iterates_shift line 128
  17. lemma OAI.DirectionalZeroOne.nthCommonList_data line 135
  18. lemma OAI.DirectionalZeroOne.nthCommonList_append line 142
  19. lemma OAI.DirectionalZeroOne.appendTapeList_prefix line 171
  20. lemma OAI.DirectionalZeroOne.listTotal_append line 179
  21. lemma OAI.DirectionalZeroOne.listTotal_reverse line 186
  22. lemma OAI.DirectionalZeroOne.iid_lintegral_sum line 190
  23. lemma OAI.DirectionalZeroOne.iid_radius_large line 199
  24. lemma OAI.DirectionalZeroOne.tapeList_ext line 223
  25. lemma OAI.DirectionalZeroOne.reverseTapeList_append line 231
  26. lemma OAI.DirectionalZeroOne.slice_sum line 237
  27. lemma OAI.DirectionalZeroOne.reverseSlice_departure line 243
  28. lemma OAI.DirectionalZeroOne.forwardSlice_departure line 263
  29. lemma OAI.DirectionalZeroOne.common_iterate_positive line 283
  30. lemma OAI.DirectionalZeroOne.common_iterate_exists line 290
  31. lemma OAI.DirectionalZeroOne.nthCommon_length_add line 297