OAI/Probability/FKMaps/WalkBounds.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.FKCRT.TreeCoding.martingale_square_submartingale line 10
  2. lemma OAI.FKCRT.TreeCoding.martingale_maximal_square_bound line 23
  3. lemma OAI.FKCRT.TreeCoding.independent_sum_martingale line 56
  4. lemma OAI.FKCRT.TreeCoding.independent_sum_second_moment line 91
  5. lemma OAI.FKCRT.TreeCoding.independent_sum_maximal_bound line 111
  6. lemma OAI.FKCRT.TreeCoding.memLp_integrable_pow_le line 135
  7. lemma OAI.FKCRT.TreeCoding.independent_add_fourth_moment line 143
  8. lemma OAI.FKCRT.TreeCoding.independent_sum_fourth_moment_bound line 182
  9. lemma OAI.FKCRT.TreeCoding.martingale_fourth_submartingale line 219
  10. lemma OAI.FKCRT.TreeCoding.martingale_maximal_fourth_bound line 232
  11. lemma OAI.FKCRT.TreeCoding.independent_sum_maximal_fourth_bound line 266
  12. lemma OAI.FKCRT.TreeCoding.block_maximal_fourth_bound line 293
  13. lemma OAI.FKCRT.TreeCoding.block_oscillation_bound line 325
  14. def OAI.FKCRT.TreeCoding.hat line 373
  15. def OAI.FKCRT.TreeCoding.interpolation line 379
  16. lemma OAI.FKCRT.TreeCoding.tent_sum_eq_one line 383
  17. lemma OAI.FKCRT.TreeCoding.hat_nonneg line 413
  18. lemma OAI.FKCRT.TreeCoding.hat_sum line 416
  19. lemma OAI.FKCRT.TreeCoding.hat_support line 425
  20. lemma OAI.FKCRT.TreeCoding.interpolation_apply line 436
  21. lemma OAI.FKCRT.TreeCoding.interpolation_sub_const_bound line 441
  22. lemma OAI.FKCRT.TreeCoding.interpolation_two_point_bound line 461
  23. lemma OAI.FKCRT.TreeCoding.interpolation_diff_bound line 474
  24. lemma OAI.FKCRT.TreeCoding.block_anchor_bound line 488
  25. lemma OAI.FKCRT.TreeCoding.block_grid_bound line 504
  26. lemma OAI.FKCRT.TreeCoding.div_diff_le_two line 523
  27. lemma OAI.FKCRT.TreeCoding.interpolation_block_modulus line 532
  28. def OAI.FKCRT.TreeCoding.tailValue line 568
  29. def OAI.FKCRT.TreeCoding.centeredTail line 571
  30. lemma OAI.FKCRT.TreeCoding.measurable_tailValue line 576
  31. lemma OAI.FKCRT.TreeCoding.tailValue_sq_le line 581
  32. lemma OAI.FKCRT.TreeCoding.tailValue_memLp line 586
  33. lemma OAI.FKCRT.TreeCoding.centeredTail_memLp line 598
  34. lemma OAI.FKCRT.TreeCoding.centeredTail_integral line 604
  35. lemma OAI.FKCRT.TreeCoding.centeredTail_second_moment_le line 611
  36. lemma OAI.FKCRT.TreeCoding.tail_second_moment_tendsto_zero line 622
  37. lemma OAI.FKCRT.TreeCoding.centeredTail_second_moment_tendsto_zero line 640
  38. def OAI.FKCRT.TreeCoding.centeredHead line 648
  39. lemma OAI.FKCRT.TreeCoding.head_abs_le line 653
  40. lemma OAI.FKCRT.TreeCoding.centeredHead_abs_le line 660
  41. lemma OAI.FKCRT.TreeCoding.centered_head_tail line 670
  42. lemma OAI.FKCRT.TreeCoding.independent_sum_scaled_maximal_bound line 680
  43. lemma OAI.FKCRT.TreeCoding.independent_centeredTail line 698
  44. lemma OAI.FKCRT.TreeCoding.centeredTail_scaled_maximal_bound line 705
  45. def OAI.FKCRT.TreeCoding.scaledWalk line 722
  46. lemma OAI.FKCRT.TreeCoding.scaledWalk_measurable line 726
  47. lemma OAI.FKCRT.TreeCoding.sum_range_block line 737
  48. lemma OAI.FKCRT.TreeCoding.grid_blocks_parameters line 744
  49. lemma OAI.FKCRT.TreeCoding.scaledWalk_modulus_bound line 762
  50. lemma OAI.FKCRT.TreeCoding.scaledWalk_maximal_bound line 794
  51. lemma OAI.FKCRT.TreeCoding.centeredHead_measurable line 823
  52. lemma OAI.FKCRT.TreeCoding.centeredHead_memLp line 828
  53. lemma OAI.FKCRT.TreeCoding.centeredHead_integral line 835
  54. lemma OAI.FKCRT.TreeCoding.centeredHead_moment_bound line 844
  55. lemma OAI.FKCRT.TreeCoding.independent_centeredHead line 855
  56. lemma OAI.FKCRT.TreeCoding.scaledWalk_add line 862
  57. lemma OAI.FKCRT.TreeCoding.scaledWalk_head_tail line 869
  58. lemma OAI.FKCRT.TreeCoding.path_modulus_add_le line 880
  59. lemma OAI.FKCRT.TreeCoding.finiteVariance_scaledWalk_modulus_bound line 891
  60. theorem OAI.FKCRT.TreeCoding.iid_scaledWalk_modulus line 927
  61. def OAI.FKCRT.TreeCoding.gridPoint line 959
  62. def OAI.FKCRT.TreeCoding.pathApprox line 969
  63. lemma OAI.FKCRT.TreeCoding.continuous_interpolation line 973
  64. lemma OAI.FKCRT.TreeCoding.continuous_pathApprox line 978
  65. lemma OAI.FKCRT.TreeCoding.hat_gridPoint_dist line 983
  66. lemma OAI.FKCRT.TreeCoding.pathApprox_error_le line 993
  67. lemma OAI.FKCRT.TreeCoding.pathApprox_tendsto line 1003
  68. lemma OAI.FKCRT.TreeCoding.pathApprox_error_event line 1016