OAI/Probability/DirectionalWalk/Widths.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalZeroOne.slabRecords line 12
  2. def OAI.DirectionalZeroOne.slabWidth line 15
  3. lemma OAI.DirectionalZeroOne.slabRecords_firstWord line 18
  4. lemma OAI.DirectionalZeroOne.slabRecords_tail line 24
  5. lemma OAI.DirectionalZeroOne.lintegral_slabRecords_le line 42
  6. lemma OAI.DirectionalZeroOne.integrable_slabRecords line 62
  7. lemma OAI.DirectionalZeroOne.height_stepVector_le_one line 73
  8. lemma OAI.DirectionalZeroOne.height_le_recordCount line 79
  9. lemma OAI.DirectionalZeroOne.slabWidth_bounds line 108
  10. lemma OAI.DirectionalZeroOne.integrable_slabWidth line 120
  11. lemma OAI.DirectionalZeroOne.lintegral_slabWidth_le line 130
  12. lemma OAI.DirectionalZeroOne.integral_slabWidth_pos line 140
  13. lemma OAI.DirectionalZeroOne.nonneg_sum_range_mono line 156
  14. lemma OAI.DirectionalZeroOne.greedy_interval_bound line 160
  15. def OAI.DirectionalZeroOne.initialAverageBad line 211
  16. lemma OAI.DirectionalZeroOne.measurableSet_initialAverageBad line 214
  17. lemma OAI.DirectionalZeroOne.integral_comp_preserving line 224
  18. lemma OAI.DirectionalZeroOne.stationary_initial_average_bound line 231