OAI/Probability/LatticePassage/ExponentialMoment.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CompanionFPP.weighted_exponential_density line 11
2. theorem OAI.CompanionFPP.exponential_laplace_five line 29
3. theorem OAI.CompanionFPP.edge_set_laplace line 38
4. lemma OAI.CompanionFPP.edge_set_exp_sum line 53
5. theorem OAI.CompanionFPP.edge_set_sum_laplace line 63
6. theorem OAI.CompanionFPP.cheap_edge_set_probability line 69