OAI/Probability/DirectionalWalk/Records.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalZeroOne.height_sub line 12
  2. def OAI.DirectionalZeroOne.recordCount line 16
  3. lemma OAI.DirectionalZeroOne.recordCount_zero line 19
  4. lemma OAI.DirectionalZeroOne.recordCount_succ line 23
  5. lemma OAI.DirectionalZeroOne.recordCount_mono line 33
  6. lemma OAI.DirectionalZeroOne.recordCount_prefix line 39
  7. lemma OAI.DirectionalZeroOne.measurable_recordCount line 50
  8. lemma OAI.DirectionalZeroOne.recordCount_strict line 59
  9. lemma OAI.DirectionalZeroOne.recordCount_boundary_unique line 65
  10. lemma OAI.DirectionalZeroOne.unbounded_recordCount line 75
  11. lemma OAI.DirectionalZeroOne.exists_record_index line 85
  12. def OAI.DirectionalZeroOne.relativeTail line 106
  13. lemma OAI.DirectionalZeroOne.relativeTail_apply line 109
  14. lemma OAI.DirectionalZeroOne.relativeTail_zero line 112
  15. lemma OAI.DirectionalZeroOne.measurable_relativeTail line 115
  16. lemma OAI.DirectionalZeroOne.strictRecord_relativeTail line 121
  17. lemma OAI.DirectionalZeroOne.trueCut_relativeTail line 143
  18. lemma OAI.DirectionalZeroOne.recordCount_relativeTail line 149
  19. def OAI.DirectionalZeroOne.noCutBeforeRecord line 160
  20. lemma OAI.DirectionalZeroOne.measurableSet_noCutBeforeRecord line 163
  21. lemma OAI.DirectionalZeroOne.noCutBeforeRecord_iff line 169
  22. def OAI.DirectionalZeroOne.recordPrefix line 181
  23. lemma OAI.DirectionalZeroOne.recordPrefix_prefix line 185
  24. lemma OAI.DirectionalZeroOne.recordPrefix_unique line 191
  25. lemma OAI.DirectionalZeroOne.measurableSet_recordPrefix line 195
  26. lemma OAI.DirectionalZeroOne.relativeTail_nonBacktracking_iff line 203
  27. lemma OAI.DirectionalZeroOne.recordPrefix_tail_subset_nonBacktracking line 207
  28. lemma OAI.DirectionalZeroOne.relativeTail_cylinder line 217
  29. lemma OAI.DirectionalZeroOne.conditioned_recordCylinder line 221
  30. lemma OAI.DirectionalZeroOne.conditioned_recordPrefix line 243
  31. def OAI.DirectionalZeroOne.reachRecord line 273
  32. def OAI.DirectionalZeroOne.recordTailEvent line 276
  33. lemma OAI.DirectionalZeroOne.measurableSet_reachRecord line 279
  34. lemma OAI.DirectionalZeroOne.measurableSet_recordTailEvent line 282
  35. lemma OAI.DirectionalZeroOne.recordPrefix_disjoint line 287
  36. lemma OAI.DirectionalZeroOne.recordTail_factorization line 295
  37. lemma OAI.DirectionalZeroOne.reachRecord_mass_ge line 305
  38. lemma OAI.DirectionalZeroOne.recordTailEvent_disjoint line 319
  39. lemma OAI.DirectionalZeroOne.record_tail_sum_bound line 347
  40. lemma OAI.DirectionalZeroOne.lintegral_nat_tail line 369