OAI/Probability/DirectionalWalk/RadiusTails.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalZeroOne.heightEnvelope line 12
  2. lemma OAI.DirectionalZeroOne.measurableSet_heightEnvelope line 15
  3. lemma OAI.DirectionalZeroOne.heightEnvelope_mono line 23
  4. lemma OAI.DirectionalZeroOne.exists_heightEnvelope_probability line 29
  5. lemma OAI.DirectionalZeroOne.indepFun_initial_block line 53
  6. def OAI.DirectionalZeroOne.prefixSum line 63
  7. lemma OAI.DirectionalZeroOne.prefixSum_eq line 66
  8. lemma OAI.DirectionalZeroOne.initial_block_factorization line 77
  9. def OAI.DirectionalZeroOne.goodRadiusTuple line 86
  10. def OAI.DirectionalZeroOne.goodRadiusPrefix line 91
  11. lemma OAI.DirectionalZeroOne.goodRadiusPrefix_iff line 94
  12. lemma OAI.DirectionalZeroOne.measurableSet_goodRadiusPrefix line 106
  13. lemma OAI.DirectionalZeroOne.goodRadiusPrefix_mono line 111
  14. lemma OAI.DirectionalZeroOne.slab_truncated_average_bound line 117
  15. lemma OAI.DirectionalZeroOne.goodRadiusPrefix_probability line 134
  16. lemma OAI.DirectionalZeroOne.goodRadiusPrefix_current_factorization line 161
  17. lemma OAI.DirectionalZeroOne.truncatedMoment_sub_le_tail line 178
  18. lemma OAI.DirectionalZeroOne.mul_tail_le_truncatedMoment_sub line 202
  19. lemma OAI.DirectionalZeroOne.truncatedMoment_zero line 225
  20. lemma OAI.DirectionalZeroOne.tail_sum_lower line 230
  21. lemma OAI.DirectionalZeroOne.tail_sum_upper line 246
  22. lemma OAI.DirectionalZeroOne.summable_real_tail_of_integrable line 259
  23. lemma OAI.DirectionalZeroOne.union_lower_of_pair_bounds line 271
  24. lemma OAI.DirectionalZeroOne.controlled_occurrence_lower line 302
  25. lemma OAI.DirectionalZeroOne.truncatedMoment_add_measure line 320
  26. lemma OAI.DirectionalZeroOne.tail_sum_Ico_lower line 327
  27. def OAI.DirectionalZeroOne.largeRadiusWord line 340
  28. lemma OAI.DirectionalZeroOne.largeRadius_mass_bounds line 343
  29. lemma OAI.DirectionalZeroOne.largeRadius_mass_pair_lower line 375
  30. lemma OAI.DirectionalZeroOne.largeRadius_mass_pair_upper line 408
  31. lemma OAI.DirectionalZeroOne.slabs_event_measureReal line 429
  32. lemma OAI.DirectionalZeroOne.slabs_pair_event_factorization line 438