OAI/Probability/FirstPassage/PositiveMoment.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarFPP.positive_weighted_density line 10
2. theorem OAI.PlanarFPP.exponential_moment_half line 28
3. theorem OAI.PlanarFPP.edge_set_positive_moment line 40
4. lemma OAI.PlanarFPP.positive_exp_sum line 56
5. theorem OAI.PlanarFPP.costly_edge_set_probability line 66