OAI/Probability/Ballisticity/Estimates/SymmetricTruncate.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.abs_supporting line 12
  2. lemma OAI.DirectionalTransience.max_square_increment line 19
  3. lemma OAI.DirectionalTransience.partialSumMax_pathwise line 25
  4. lemma OAI.DirectionalTransience.partialSumMax_square_pathwise line 40
  5. lemma OAI.DirectionalTransience.measurable_realPartialSum line 46
  6. lemma OAI.DirectionalTransience.measurable_partialSumMax line 51
  7. lemma OAI.DirectionalTransience.measurable_absSlope line 57
  8. lemma OAI.DirectionalTransience.integrable_of_abs_bound line 60
  9. lemma OAI.DirectionalTransience.realPartialSum_congr line 65
  10. lemma OAI.DirectionalTransience.partialSumMax_congr line 69
  11. lemma OAI.DirectionalTransience.independent_max_transform line 77
  12. lemma OAI.DirectionalTransience.integrable_partialSumMax_square line 96
  13. lemma OAI.DirectionalTransience.integrable_realPartialSum_square line 105
  14. lemma OAI.DirectionalTransience.integral_partialSumMax_square_le line 117
  15. lemma OAI.DirectionalTransience.integral_partialSum_square_eq_sum line 146
  16. lemma OAI.DirectionalTransience.integral_partialSumMax_square_le_sum line 168
  17. def OAI.DirectionalTransience.symmetricTruncate line 177
  18. def OAI.DirectionalTransience.truncatedTailCost line 178
  19. lemma OAI.DirectionalTransience.measurable_symmetricTruncate line 180
  20. lemma OAI.DirectionalTransience.measurable_truncatedTailCost line 183
  21. lemma OAI.DirectionalTransience.symmetricTruncate_bound line 186
  22. lemma OAI.DirectionalTransience.symmetricTruncate_neg line 192
  23. lemma OAI.DirectionalTransience.symmetricTruncate_sq_le line 196
  24. lemma OAI.DirectionalTransience.truncatedTailCost_nonneg line 202
  25. lemma OAI.DirectionalTransience.truncatedTailCost_le line 206
  26. lemma OAI.DirectionalTransience.integral_symmetricTruncate_zero line 213
  27. lemma OAI.DirectionalTransience.capped_partialSumMax_le_truncated line 221
  28. lemma OAI.DirectionalTransience.integral_partialSumMax_capped_le line 241
  29. lemma OAI.DirectionalTransience.measureReal_partialSumMax_gt_le line 294
  30. def OAI.DirectionalTransience.commonIncrementProcess line 323
  31. lemma OAI.DirectionalTransience.measurable_commonIncrementProcess line 327
  32. lemma OAI.DirectionalTransience.commonIncrements_independent line 332
  33. lemma OAI.DirectionalTransience.commonIncrements_identDistrib line 340
  34. lemma OAI.DirectionalTransience.independent_common_maximal_capped line 348
  35. lemma OAI.DirectionalTransience.independent_common_maximal_probability line 365
  36. lemma OAI.DirectionalTransience.signedCoordinate_sub line 383
  37. lemma OAI.DirectionalTransience.commonTimes_span line 388
  38. lemma OAI.DirectionalTransience.common_coordinate_sum line 405
  39. lemma OAI.DirectionalTransience.commonIndex_le_recordCount line 420