OAI/Probability/LatticePassage/NaturalMoment.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CompanionFPP.exponential_nat_moment_density line 8
2. theorem OAI.CompanionFPP.exponential_nat_lmoment line 23
3. theorem OAI.CompanionFPP.integrable_exponential_pow line 33
4. theorem OAI.CompanionFPP.integral_exponential_pow line 40
5. lemma OAI.CompanionFPP.integrable_edge_weight line 47
6. lemma OAI.CompanionFPP.integral_edge_weight line 53
7. theorem OAI.CompanionFPP.integral_pathCost line 62
8. theorem OAI.CompanionFPP.mean_passageTime_le_distance line 77