OAI/Probability/Ballisticity/Estimates/MartingaleExponentialSubmartingale.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.DirectionalTransience.martingale_exponential_submartingaleline 288 - lemma
OAI.DirectionalTransience.martingale_exponential_maximalline 300 - lemma
OAI.DirectionalTransience.gaussian_martingale_maximalline 333 - lemma
OAI.DirectionalTransience.gaussian_martingale_abs_maximalline 362 - lemma
OAI.DirectionalTransience.independent_centered_sum_martingaleline 389