OAI/Probability/Ballisticity/Estimates/VarianceTailDifference.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.truncated_variance_tail_difference line 14
2. lemma OAI.DirectionalTransience.fluctuation_tail_difference line 40
3. lemma OAI.DirectionalTransience.dyadicCut_add line 54
4. lemma OAI.DirectionalTransience.dyadicCut_succ line 56
5. lemma OAI.DirectionalTransience.dyadic_profile_gaussian_tail line 70
6. lemma OAI.DirectionalTransience.isGaussianSequence_of_dyadic line 103
7. lemma OAI.DirectionalTransience.double_gaussian_selection line 129