OAI/Probability/DirectionalWalk/RadiusLaunch.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalZeroOne.controlledSlabOccurrence line 12
  2. lemma OAI.DirectionalZeroOne.measurableSet_controlledSlabOccurrence line 16
  3. lemma OAI.DirectionalZeroOne.controlledSlabOccurrence_probability line 25
  4. lemma OAI.DirectionalZeroOne.controlledSlabOccurrence_probability_half line 53
  5. lemma OAI.DirectionalZeroOne.slabWidth_pos_of_regeneration line 66
  6. lemma OAI.DirectionalZeroOne.slabHeightSum_strictMono line 71
  7. lemma OAI.DirectionalZeroOne.slabHeightSum_nonneg line 79
  8. lemma OAI.DirectionalZeroOne.slabRadiusSum_mono line 83
  9. lemma OAI.DirectionalZeroOne.goodSlabPath_height_nonneg line 88
  10. lemma OAI.DirectionalZeroOne.height_before_slabTime_le line 96
  11. lemma OAI.DirectionalZeroOne.height_after_slabTime_le line 108
  12. lemma OAI.DirectionalZeroOne.norm_before_slabTime_le line 120
  13. def OAI.DirectionalZeroOne.stepDirection line 133
  14. lemma OAI.DirectionalZeroOne.height_stepDirection line 135
  15. lemma OAI.DirectionalZeroOne.height_stepDirection_le_norm line 142
  16. lemma OAI.DirectionalZeroOne.exists_large_signedCoordinate line 148
  17. def OAI.DirectionalZeroOne.tiltDirection line 172
  18. lemma OAI.DirectionalZeroOne.height_tiltDirection line 175
  19. lemma OAI.DirectionalZeroOne.largeRadius_point line 183
  20. def OAI.DirectionalZeroOne.radiusLaunch line 204
  21. lemma OAI.DirectionalZeroOne.measurableSet_radiusLaunch line 211
  22. lemma OAI.DirectionalZeroOne.radiusLaunch_prefix line 225
  23. lemma OAI.DirectionalZeroOne.first_crossing_strictRecord line 232
  24. lemma OAI.DirectionalZeroOne.largeRadius_launch line 246
  25. lemma OAI.DirectionalZeroOne.height_signed_step_abs_le_one line 284
  26. lemma OAI.DirectionalZeroOne.tilt_down_step_lower line 289
  27. lemma OAI.DirectionalZeroOne.radius_script_fresh line 296
  28. lemma OAI.DirectionalZeroOne.opposite_template_height line 308
  29. lemma OAI.DirectionalZeroOne.radius_template_before line 314
  30. lemma OAI.DirectionalZeroOne.radius_template_avoids line 339
  31. lemma OAI.DirectionalZeroOne.radius_continuation_maximum line 373
  32. lemma OAI.DirectionalZeroOne.measure_prefix_lower line 402
  33. lemma OAI.DirectionalZeroOne.measure_first_prefix_lower line 426