OAI/Probability/Ballisticity/Estimates/IntegerMedian.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.integerMedian line 12
  2. lemma OAI.DirectionalTransience.integerMedian_spec line 15
  3. lemma OAI.DirectionalTransience.median_family_symmetrization line 20
  4. def OAI.DirectionalTransience.signedIntegerCoordinate line 64
  5. lemma OAI.DirectionalTransience.signedIntegerCoordinate_cast line 67
  6. def OAI.DirectionalTransience.recordMedian line 72
  7. lemma OAI.DirectionalTransience.recordMedian_spec line 81
  8. lemma OAI.DirectionalTransience.conditioned_firstHit_median_maximum line 99
  9. def OAI.DirectionalTransience.IsGaussianSequence line 121
  10. lemma OAI.DirectionalTransience.one_sub_cos_sinc line 127
  11. lemma OAI.DirectionalTransience.cosine_quadratic_local line 139
  12. lemma OAI.DirectionalTransience.truncatedVariance_div line 159
  13. lemma OAI.DirectionalTransience.gaussian_quadratic_integral line 168
  14. lemma OAI.DirectionalTransience.gaussian_cosine_limit line 253
  15. lemma OAI.DirectionalTransience.symmetric_sine_integral line 265
  16. lemma OAI.DirectionalTransience.symmetric_charFun_cosine line 272
  17. lemma OAI.DirectionalTransience.gaussian_cosine_drift line 291
  18. lemma OAI.DirectionalTransience.tendsto_pow_variable_of_drift line 305
  19. lemma OAI.DirectionalTransience.gaussian_cosine_power_limit line 324
  20. lemma OAI.DirectionalTransience.gaussian_charFun_power_limit line 354
  21. lemma OAI.DirectionalTransience.charFun_div_partialSum line 372
  22. theorem OAI.DirectionalTransience.gaussian_iid_marginal_limit line 383
  23. theorem OAI.DirectionalTransience.independent_common_gaussian_marginal line 406