OAI/Probability/LatticePassage/PassageVariance.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CompanionFPP.integrable_finitePassageTime line 11
2. theorem OAI.CompanionFPP.finitePassageTime_centered_lmoment line 22
3. lemma OAI.CompanionFPP.finitePassageTime_mean line 35
4. theorem OAI.CompanionFPP.localPassageTime_centered_lmoment line 46
5. lemma OAI.CompanionFPP.centered_square_markov line 66
6. lemma OAI.CompanionFPP.sqrt_scale_ratio line 80
7. theorem OAI.CompanionFPP.finitePassageTime_centered_sqrt_tail line 86
8. theorem OAI.CompanionFPP.localPassageTime_centered_sqrt_tail line 101