OAI/Probability/LatticePassage/PositiveMoment.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CompanionFPP.positive_weighted_density line 9
2. theorem OAI.CompanionFPP.exponential_moment_half line 27
3. theorem OAI.CompanionFPP.edge_set_positive_moment line 37
4. lemma OAI.CompanionFPP.positive_exp_sum line 52
5. theorem OAI.CompanionFPP.costly_edge_set_probability line 62
6. theorem OAI.CompanionFPP.costly_trail_probability line 81