OAI/Probability/DirectionalWalk/Axis.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalZeroOne.axisDirection line 12
  2. def OAI.DirectionalZeroOne.axisHeight line 15
  3. lemma OAI.DirectionalZeroOne.height_axisDirection line 18
  4. lemma OAI.DirectionalZeroOne.axisHeight_zero line 23
  5. lemma OAI.DirectionalZeroOne.axisDirection_ne_zero line 26
  6. lemma OAI.DirectionalZeroOne.axisDirection_normalized line 32
  7. lemma OAI.DirectionalZeroOne.axisHeight_add line 43
  8. lemma OAI.DirectionalZeroOne.axisHeight_step_le line 48
  9. lemma OAI.DirectionalZeroOne.axisHeight_step_ge line 53
  10. lemma OAI.DirectionalZeroOne.axisHeight_nn_le line 58
  11. lemma OAI.DirectionalZeroOne.axis_recordCount_witness line 64
  12. lemma OAI.DirectionalZeroOne.axis_record_height line 82
  13. lemma OAI.DirectionalZeroOne.integer_first_crossing line 106
  14. def OAI.DirectionalZeroOne.reachAxis line 126
  15. lemma OAI.DirectionalZeroOne.measurableSet_reachAxis line 129
  16. lemma OAI.DirectionalZeroOne.reachRecord_eq_reachAxis line 136
  17. lemma OAI.DirectionalZeroOne.reachAxis_antitone line 165
  18. lemma OAI.DirectionalZeroOne.last_record_cut_partition line 174
  19. lemma OAI.DirectionalZeroOne.record_tail_sum_eq_one line 208
  20. def OAI.DirectionalZeroOne.axisReachProb line 234
  21. lemma OAI.DirectionalZeroOne.axisReachProb_eq_record line 237
  22. lemma OAI.DirectionalZeroOne.axisReachProb_antitone line 243
  23. lemma OAI.DirectionalZeroOne.axisReachProb_lower line 250
  24. lemma OAI.DirectionalZeroOne.axisReachProb_zero line 256
  25. def OAI.DirectionalZeroOne.axisWidthTail line 265
  26. lemma OAI.DirectionalZeroOne.axis_renewal_tail_identity line 269
  27. lemma OAI.DirectionalZeroOne.slabRecords_pos line 277
  28. lemma OAI.DirectionalZeroOne.axis_slabWidth_eq_records line 284
  29. lemma OAI.DirectionalZeroOne.axisWidthTail_zero line 296
  30. lemma OAI.DirectionalZeroOne.axisWidthTail_antitone line 304
  31. lemma OAI.DirectionalZeroOne.renewal_step_bound line 309
  32. lemma OAI.DirectionalZeroOne.renewal_interval_bound line 326
  33. lemma OAI.DirectionalZeroOne.axis_renewal_identity_real line 341
  34. lemma OAI.DirectionalZeroOne.axis_renewal_tail_bound line 352
  35. lemma OAI.DirectionalZeroOne.summable_axisWidthTail line 370
  36. lemma OAI.DirectionalZeroOne.summable_dyadic_axisWidthTail line 380
  37. lemma OAI.DirectionalZeroOne.iterated_cutSuffix_eq_relativeTail line 389
  38. lemma OAI.DirectionalZeroOne.slabTime_boundary line 394
  39. lemma OAI.DirectionalZeroOne.trueCut_eq_slabTime line 408
  40. lemma OAI.DirectionalZeroOne.recordCount_slabTime line 426
  41. def OAI.DirectionalZeroOne.tapeCut line 438
  42. lemma OAI.DirectionalZeroOne.measurableSet_tapeCut line 441
  43. lemma OAI.DirectionalZeroOne.tapeCut_iff_recordTailEvent line 449
  44. lemma OAI.DirectionalZeroOne.tapeCut_mass line 476
  45. lemma OAI.DirectionalZeroOne.axis_tapeCut_mass line 491