OAI/Analysis/HardSphere/PathBounds/ExpNatTail.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.FreeVisits.exp_block_sum_bound line 12
2. lemma OAI.HardSphere.FreeVisits.weighted_exp_tail_le line 35
3. def OAI.HardSphere.FreeVisits.expTailBound line 49
4. lemma OAI.HardSphere.FreeVisits.expTailBound_ne_top line 53
5. lemma OAI.HardSphere.FreeVisits.lintegral_exp_nat_le line 62
6. def OAI.HardSphere.FreeVisits.visitWeight line 120
7. lemma OAI.HardSphere.FreeVisits.visitWeight_measurable line 124
8. lemma OAI.HardSphere.FreeVisits.exp_nat_sum_le line 128
9. lemma OAI.HardSphere.FreeVisits.visit_moment_add line 137
10. lemma OAI.HardSphere.FreeVisits.n_segment_visit_moment line 173
11. lemma OAI.HardSphere.FreeVisits.small_visit_moment line 187
12. theorem OAI.HardSphere.FreeVisits.free_visit_moment line 211