OAI/Probability/DirectionalWalk/RadiusMoment.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalZeroOne.finiteHighMaximum line 12
  2. lemma OAI.DirectionalZeroOne.measurableSet_finiteHighMaximum line 15
  3. lemma OAI.DirectionalZeroOne.finiteHighMaximum_mono line 22
  4. lemma OAI.DirectionalZeroOne.tendsto_measure_finiteHighMaximum line 27
  5. lemma OAI.DirectionalZeroOne.measurableSet_goodSlabPath line 44
  6. def OAI.DirectionalZeroOne.radiusTemplate line 51
  7. lemma OAI.DirectionalZeroOne.measurableSet_radiusTemplate line 54
  8. lemma OAI.DirectionalZeroOne.annealed_radiusTemplate line 58
  9. lemma OAI.DirectionalZeroOne.shiftPath_add_neg_cancel line 76
  10. lemma OAI.DirectionalZeroOne.shiftPath_neg_add_cancel line 81
  11. lemma OAI.DirectionalZeroOne.annealed_translated_event line 86
  12. lemma OAI.DirectionalZeroOne.radius_launch_cylinder_lower line 97
  13. lemma OAI.DirectionalZeroOne.radius_launch_probability_lower line 154
  14. lemma OAI.DirectionalZeroOne.controlledSlabOccurrence_launch line 168
  15. lemma OAI.DirectionalZeroOne.annealed_goodSlabPath_event line 188
  16. lemma OAI.DirectionalZeroOne.radius_occurrence_probability_upper line 206
  17. lemma OAI.DirectionalZeroOne.radius_occurrence_mass_le line 246
  18. lemma OAI.DirectionalZeroOne.goodRadiusPrefix_uniform_probability line 287
  19. lemma OAI.DirectionalZeroOne.summable_real_upper_tail line 304
  20. lemma OAI.DirectionalZeroOne.summable_small_Ico line 311
  21. lemma OAI.DirectionalZeroOne.measurable_slabHeightSum line 320
  22. lemma OAI.DirectionalZeroOne.exists_common_heightEnvelope line 327
  23. lemma OAI.DirectionalZeroOne.truncatedMoment_component_scale line 361
  24. lemma OAI.DirectionalZeroOne.tendsto_real_finiteHighMaximum line 380
  25. lemma OAI.DirectionalZeroOne.meanStep_power_real_pos line 385
  26. lemma OAI.DirectionalZeroOne.integrable_radius_from_parameters line 390
  27. lemma OAI.DirectionalZeroOne.exists_down_unit_step line 535
  28. lemma OAI.DirectionalZeroOne.integrable_slabRadius_normalized line 544