OAI/Probability/Ballisticity/Estimates/TruncatedVarianceDouble.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.truncatedVariance_double_le line 258
2. lemma OAI.DirectionalTransience.good_scale_doubling line 284
3. lemma OAI.DirectionalTransience.good_scale_dyadic line 307
4. lemma OAI.DirectionalTransience.good_scale_power_bound line 333
5. lemma OAI.DirectionalTransience.fluctuationScale_upper_ratio line 368
6. theorem OAI.DirectionalTransience.good_scale_comparison line 383