OAI/Probability/LatticePassage/DirectionalConvergence.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CompanionFPP.exp_neg_sqrt_le line 11
2. lemma OAI.CompanionFPP.summable_exp_neg_sqrt line 23
3. lemma OAI.CompanionFPP.directional_centered_tail line 31
4. lemma OAI.CompanionFPP.ae_directional_centered_small line 58
5. theorem OAI.CompanionFPP.passageTime_directional_tendsto line 78
6. theorem OAI.CompanionFPP.passageTime_all_directions_tendsto line 115