OAI/Probability/Ballisticity/Geometry/SignedHeight.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.signedHeight line 12
  2. lemma OAI.DirectionalTransience.signedHeight_projection line 15
  3. lemma OAI.DirectionalTransience.signedHeight_step_le line 20
  4. theorem OAI.DirectionalTransience.transverse_common_gaussian_marginal line 25
  5. lemma OAI.DirectionalTransience.max_fourth_increment line 42
  6. lemma OAI.DirectionalTransience.partialSumMax_fourth_pathwise line 51
  7. lemma OAI.DirectionalTransience.partialSumMax_fourth_pathwise_bound line 67
  8. lemma OAI.DirectionalTransience.integrable_partialSumMax_pow line 78
  9. lemma OAI.DirectionalTransience.integrable_realPartialSum_pow line 87
  10. lemma OAI.DirectionalTransience.absSlope_cube line 97
  11. lemma OAI.DirectionalTransience.independent_max_cube_transform line 101
  12. lemma OAI.DirectionalTransience.integral_partialSumMax_fourth_le line 109
  13. lemma OAI.DirectionalTransience.independent_partialSum_current line 139
  14. lemma OAI.DirectionalTransience.integrable_pow_mul_of_abs_bound line 149
  15. lemma OAI.DirectionalTransience.integral_independent_add_fourth line 161
  16. lemma OAI.DirectionalTransience.integral_iid_partialSum_fourth_le line 192
  17. lemma OAI.DirectionalTransience.integral_iid_truncated_max_fourth_le line 223
  18. lemma OAI.DirectionalTransience.measureReal_truncated_max_gt_le line 266
  19. lemma OAI.DirectionalTransience.measureReal_iid_max_gt_fourth_bound line 292
  20. lemma OAI.DirectionalTransience.gaussian_charFun_power_limit_count line 328
  21. lemma OAI.DirectionalTransience.charFun_independent_finite_blocks line 366
  22. theorem OAI.DirectionalTransience.gaussian_iid_finite_block_limit line 405