OAI/Probability/Ballisticity/Geometry/SignedCoordinate.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.conditioned_rare_word_template_lower line 12
  2. lemma OAI.DirectionalTransience.large_regeneration_word_excursion line 57
  3. def OAI.DirectionalTransience.signedCoordinate line 95
  4. lemma OAI.DirectionalTransience.signedCoordinate_add line 98
  5. lemma OAI.DirectionalTransience.signedCoordinate_abs_le_norm line 103
  6. lemma OAI.DirectionalTransience.latticeVector_norm_le_sum_abs line 109
  7. lemma OAI.DirectionalTransience.exists_large_signedCoordinate line 118
  8. lemma OAI.DirectionalTransience.prefixMax_mono line 130
  9. lemma OAI.DirectionalTransience.prefixMax_le_iff line 135
  10. lemma OAI.DirectionalTransience.prefixMax_congr line 150
  11. def OAI.DirectionalTransience.runningHeight line 156
  12. lemma OAI.DirectionalTransience.runningHeight_nonneg line 159
  13. lemma OAI.DirectionalTransience.height_le_runningHeight line 162
  14. lemma OAI.DirectionalTransience.runningHeight_mono line 165
  15. lemma OAI.DirectionalTransience.runningHeight_le line 168
  16. lemma OAI.DirectionalTransience.runningHeight_congr line 172
  17. lemma OAI.DirectionalTransience.measurable_runningHeight line 178
  18. def OAI.DirectionalTransience.tiltedCoordinate line 187
  19. def OAI.DirectionalTransience.heightRatio line 190
  20. lemma OAI.DirectionalTransience.tiltedCoordinate_add line 193
  21. lemma OAI.DirectionalTransience.tiltedCoordinate_zero line 198
  22. lemma OAI.DirectionalTransience.measurable_heightRatio line 201
  23. def OAI.DirectionalTransience.AdmissiblePrefix line 208
  24. def OAI.DirectionalTransience.BoundedHeightPrefix line 211
  25. def OAI.DirectionalTransience.RatioExceed line 214
  26. def OAI.DirectionalTransience.RatioHit line 217
  27. def OAI.DirectionalTransience.FirstRatioExceed line 220
  28. lemma OAI.DirectionalTransience.measurableSet_admissiblePrefix line 223
  29. lemma OAI.DirectionalTransience.measurableSet_boundedHeightPrefix line 229
  30. lemma OAI.DirectionalTransience.measurableSet_ratioExceed line 236
  31. lemma OAI.DirectionalTransience.measurableSet_ratioHit line 241
  32. lemma OAI.DirectionalTransience.measurableSet_firstRatioExceed line 245
  33. lemma OAI.DirectionalTransience.admissiblePrefix_mono line 252
  34. lemma OAI.DirectionalTransience.boundedHeightPrefix_mono line 256
  35. lemma OAI.DirectionalTransience.ratioHit_eq_first line 260
  36. lemma OAI.DirectionalTransience.firstRatioExceed_disjoint line 277
  37. lemma OAI.DirectionalTransience.ratioHit_antitone line 286
  38. lemma OAI.DirectionalTransience.firstRatioExceed_record line 292
  39. lemma OAI.DirectionalTransience.prefixDetermined_admissiblePrefix line 312
  40. lemma OAI.DirectionalTransience.prefixDetermined_boundedHeightPrefix line 324
  41. lemma OAI.DirectionalTransience.heightRatio_congr line 330
  42. lemma OAI.DirectionalTransience.prefixDetermined_firstRatioExceed line 334
  43. lemma OAI.DirectionalTransience.firstRatioExceed_overshoot line 347
  44. lemma OAI.DirectionalTransience.annealed_prefix_avoiding_suffix line 382