OAI/Probability/Ballisticity/Estimates/CommonWordIncrement.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.commonTrueRecord_swap line 12
  2. lemma OAI.DirectionalTransience.firstCommonTrueRecord_swap line 16
  3. lemma OAI.DirectionalTransience.firstPairWordEvent_swap line 28
  4. lemma OAI.DirectionalTransience.firstPairWord_swap line 37
  5. lemma OAI.DirectionalTransience.independent_commonWordRadius_snd_integrable line 55
  6. def OAI.DirectionalTransience.commonWordIncrement line 76
  7. lemma OAI.DirectionalTransience.commonWordIncrement_abs_le line 80
  8. lemma OAI.DirectionalTransience.independent_commonWordIncrement_integrable line 85
  9. lemma OAI.DirectionalTransience.independent_commonWordIncrement_symmetric line 97
  10. lemma OAI.DirectionalTransience.signedCoordinate_step_self line 119
  11. lemma OAI.DirectionalTransience.signedCoordinate_step_other line 124
  12. lemma OAI.DirectionalTransience.admissible_transverse_commonWords line 128
  13. lemma OAI.DirectionalTransience.annealed_wordCylinder_positive line 160
  14. lemma OAI.DirectionalTransience.independent_commonWordIncrement_nonzero line 167
  15. def OAI.DirectionalTransience.truncatedVariance line 191
  16. def OAI.DirectionalTransience.fluctuationScale line 193
  17. lemma OAI.DirectionalTransience.integrable_truncated_square line 196
  18. lemma OAI.DirectionalTransience.truncatedVariance_nonneg line 204
  19. lemma OAI.DirectionalTransience.truncatedVariance_pos line 208
  20. lemma OAI.DirectionalTransience.truncatedVariance_mono line 218
  21. lemma OAI.DirectionalTransience.truncatedVariance_le_sq line 225
  22. lemma OAI.DirectionalTransience.min_sq_le_mul_abs line 232
  23. lemma OAI.DirectionalTransience.truncatedVariance_le_firstMoment line 239
  24. lemma OAI.DirectionalTransience.truncatedVariance_abs_sub_le line 247
  25. lemma OAI.DirectionalTransience.continuous_truncatedVariance line 259
  26. lemma OAI.DirectionalTransience.min_sq_cross line 271
  27. lemma OAI.DirectionalTransience.fluctuationScale_mono line 283
  28. lemma OAI.DirectionalTransience.integral_abs_pos_of_nonzero line 295
  29. lemma OAI.DirectionalTransience.fluctuationScale_lower line 301
  30. lemma OAI.DirectionalTransience.fluctuationScale_scaling line 312
  31. lemma OAI.DirectionalTransience.fluctuationScale_tendsto line 323
  32. lemma OAI.DirectionalTransience.continuousOn_fluctuationScale line 332
  33. lemma OAI.DirectionalTransience.exists_bounded_nonzero line 338
  34. lemma OAI.DirectionalTransience.fluctuationScale_eventually_strictMono line 352
  35. def OAI.DirectionalTransience.realPartialSum line 388
  36. def OAI.DirectionalTransience.partialSumMax line 390
  37. lemma OAI.DirectionalTransience.realPartialSum_zero line 394
  38. lemma OAI.DirectionalTransience.realPartialSum_succ line 395
  39. lemma OAI.DirectionalTransience.partialSumMax_nonneg line 398
  40. lemma OAI.DirectionalTransience.abs_partialSum_le_max line 403
  41. lemma OAI.DirectionalTransience.partialSumMax_mono line 408
  42. lemma OAI.DirectionalTransience.partialSumMax_bound line 411
  43. def OAI.DirectionalTransience.absSlope line 424
  44. lemma OAI.DirectionalTransience.abs_absSlope line 426