OAI/Probability/Ballisticity/Estimates/AeMaximalSquare.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.integral_partialSumMax_square_le_sum_ae line 14
2. lemma OAI.DirectionalTransience.integrable_abs_sub_bounded line 50
3. lemma OAI.DirectionalTransience.abs_mean_sub_le line 60
4. lemma OAI.DirectionalTransience.integral_centered_square_le line 71
5. lemma OAI.DirectionalTransience.iidList_integral_max_square_le line 77
6. lemma OAI.DirectionalTransience.integrable_partialSumMax_pow_ae line 144
7. lemma OAI.DirectionalTransience.iidList_integrable_max_square line 153
8. lemma OAI.DirectionalTransience.iidList_max_tail line 183