OAI/Probability/DirectionalWalk/Radii.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalZeroOne.euclideanSite line 12
  2. lemma OAI.DirectionalZeroOne.euclideanSite_add line 15
  3. lemma OAI.DirectionalZeroOne.euclideanSite_zero line 20
  4. lemma OAI.DirectionalZeroOne.euclideanSite_sub line 24
  5. def OAI.DirectionalZeroOne.slabRadius line 29
  6. lemma OAI.DirectionalZeroOne.norm_wordPath_le_radius line 33
  7. lemma OAI.DirectionalZeroOne.slabRadius_nonneg line 38
  8. lemma OAI.DirectionalZeroOne.slabs_identDistrib line 41
  9. lemma OAI.DirectionalZeroOne.slabObservable_strongLaw line 50
  10. lemma OAI.DirectionalZeroOne.slabWidth_strongLaw line 69
  11. lemma OAI.DirectionalZeroOne.slab_initial_average_bound line 77
  12. def OAI.DirectionalZeroOne.slabTime line 96
  13. lemma OAI.DirectionalZeroOne.slabTime_zero line 99
  14. lemma OAI.DirectionalZeroOne.slabTime_succ line 102
  15. lemma OAI.DirectionalZeroOne.iterated_cutSuffix line 106
  16. lemma OAI.DirectionalZeroOne.slab_word_path line 120
  17. def OAI.DirectionalZeroOne.GoodSlabPath line 125
  18. lemma OAI.DirectionalZeroOne.ae_goodSlabPath line 128
  19. lemma OAI.DirectionalZeroOne.slabTime_strictMono line 142
  20. lemma OAI.DirectionalZeroOne.slab_location line 149
  21. def OAI.DirectionalZeroOne.slabHeightSum line 162
  22. def OAI.DirectionalZeroOne.slabRadiusSum line 165
  23. lemma OAI.DirectionalZeroOne.height_at_slabTime line 168
  24. lemma OAI.DirectionalZeroOne.norm_at_slabTime_le line 182
  25. lemma OAI.DirectionalZeroOne.norm_in_slab_le line 198
  26. lemma OAI.DirectionalZeroOne.height_in_slab line 212
  27. def OAI.DirectionalZeroOne.truncatedMoment line 226
  28. lemma OAI.DirectionalZeroOne.integrable_min_const line 229
  29. lemma OAI.DirectionalZeroOne.truncatedMoment_nonneg line 237
  30. lemma OAI.DirectionalZeroOne.truncatedMoment_mono line 241
  31. lemma OAI.DirectionalZeroOne.min_mul_le_mul_min line 248
  32. lemma OAI.DirectionalZeroOne.truncatedMoment_mul_le line 256
  33. lemma OAI.DirectionalZeroOne.truncatedMoment_sublinear line 266
  34. lemma OAI.DirectionalZeroOne.integrable_of_truncatedMoment_bounded line 287
  35. lemma OAI.DirectionalZeroOne.exists_truncatedMoment_gt line 314
  36. lemma OAI.DirectionalZeroOne.truncatedMoment_scaled_sublinear line 322
  37. lemma OAI.DirectionalZeroOne.exists_truncation_multiple line 334
  38. lemma OAI.DirectionalZeroOne.radius_scales line 346
  39. lemma OAI.DirectionalZeroOne.stationary_truncated_average_bound line 389
  40. lemma OAI.DirectionalZeroOne.linear_envelope_of_tendsto line 443