OAI/Probability/DirectionalWalk/DirectionalReduction.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalZeroOne.wordOffset line 12
  2. def OAI.DirectionalZeroOne.wordSequenceEscape line 15
  3. lemma OAI.DirectionalZeroOne.wordOffset_add line 18
  4. lemma OAI.DirectionalZeroOne.wordSequenceEscape_shift line 22
  5. lemma OAI.DirectionalZeroOne.measurableSet_wordSequenceEscape line 41
  6. lemma OAI.DirectionalZeroOne.wordSequenceEscape_zero_one line 49
  7. def OAI.DirectionalZeroOne.heightBound line 69
  8. lemma OAI.DirectionalZeroOne.heightBound_nonneg line 71
  9. lemma OAI.DirectionalZeroOne.abs_height_le_norm line 74
  10. def OAI.DirectionalZeroOne.slabFloor line 86
  11. lemma OAI.DirectionalZeroOne.slabFloor_le line 90
  12. lemma OAI.DirectionalZeroOne.abs_word_height_le_radius line 94
  13. lemma OAI.DirectionalZeroOne.abs_slabFloor_le_radius line 101
  14. lemma OAI.DirectionalZeroOne.height_at_slabTime_projection line 112
  15. lemma OAI.DirectionalZeroOne.height_in_slab_projection line 127
  16. lemma OAI.DirectionalZeroOne.escape_iff_wordSequenceEscape line 135
  17. lemma OAI.DirectionalZeroOne.conditioned_escape_zero_one line 173
  18. lemma OAI.DirectionalZeroOne.tendsto_term_div_nat_of_average line 187
  19. lemma OAI.DirectionalZeroOne.tendsto_atTop_of_positive_slope line 205
  20. lemma OAI.DirectionalZeroOne.relativeTail_escape_iff line 222
  21. lemma OAI.DirectionalZeroOne.annealed_shift_back line 238
  22. lemma OAI.DirectionalZeroOne.annealed_relativeTail_null line 254
  23. lemma OAI.DirectionalZeroOne.conditioned_null_transfer line 267
  24. lemma OAI.DirectionalZeroOne.conditioned_ae_transfer line 292
  25. lemma OAI.DirectionalZeroOne.integrable_slabProjection line 306
  26. lemma OAI.DirectionalZeroOne.ae_slabRadius_sublinear line 315
  27. lemma OAI.DirectionalZeroOne.conditioned_escape_of_positive_mean line 324
  28. def OAI.DirectionalZeroOne.slabMean line 346
  29. def OAI.DirectionalZeroOne.directionDot line 350
  30. lemma OAI.DirectionalZeroOne.integral_slabProjection line 352
  31. lemma OAI.DirectionalZeroOne.directionDot_add_right line 369
  32. lemma OAI.DirectionalZeroOne.directionDot_self_pos line 373
  33. lemma OAI.DirectionalZeroOne.escape_not_opposite line 384
  34. lemma OAI.DirectionalZeroOne.escape_zero_one_of_full_direction line 394
  35. lemma OAI.DirectionalZeroOne.not_zero_one_of_opposite_positive line 419
  36. lemma OAI.DirectionalZeroOne.positive_raw_of_conditioned_ae line 432
  37. lemma OAI.DirectionalZeroOne.coordinate_direction_ne_zero line 445
  38. lemma OAI.DirectionalZeroOne.exists_mixed_coordinate line 451
  39. lemma OAI.DirectionalZeroOne.height_scale_direction line 526
  40. lemma OAI.DirectionalZeroOne.escape_scale_direction line 533
  41. lemma OAI.DirectionalZeroOne.direction_normalization line 540
  42. lemma OAI.DirectionalZeroOne.mixed_direction_has_mixed_coordinate line 558