OAI/Probability/LatticePassage/SecondMoment.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CompanionFPP.integrable_edge_square line 11
2. lemma OAI.CompanionFPP.integral_edge_square line 16
3. lemma OAI.CompanionFPP.edge_memLp_two line 24
4. lemma OAI.CompanionFPP.integrable_edge_mul line 27
5. lemma OAI.CompanionFPP.integral_edge_mul line 31
6. theorem OAI.CompanionFPP.pathCost_memLp_two line 41
7. theorem OAI.CompanionFPP.trailCost_second_moment line 47
8. theorem OAI.CompanionFPP.passageTime_memLp_two line 63
9. theorem OAI.CompanionFPP.passageTime_second_moment line 71
10. theorem OAI.CompanionFPP.targetCocycle_second_moment line 84