OAI/Probability/Ballisticity/Walk/PathPointMean.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.pathPointMean line 39
2. lemma OAI.DirectionalTransience.path_finite_gaussian_marginal line 42
3. lemma OAI.DirectionalTransience.path_marginal_eq_gaussian line 56
4. lemma OAI.DirectionalTransience.continuous_pathPointMean line 68
5. lemma OAI.DirectionalTransience.path_finite_mean line 74
6. theorem OAI.DirectionalTransience.path_iid_difference_centered line 86