OAI/Probability/Renewal/SumLaw.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HoneycombLocal.pairLaw line 11
2. lemma OAI.HoneycombLocal.pairLaw_apply line 16
3. lemma OAI.HoneycombLocal.pairLaw_toMeasure line 18
4. lemma OAI.HoneycombLocal.sumLaw_succ_map line 27
5. lemma OAI.HoneycombLocal.sumLaw_transform line 40
6. lemma OAI.HoneycombLocal.latticeChar_sumLaw line 52
7. lemma OAI.HoneycombLocal.laplace_sumLaw line 62
8. lemma OAI.HoneycombLocal.sumLaw_inversion line 72
9. lemma OAI.HoneycombLocal.tail_from_laplace line 78
10. lemma OAI.HoneycombLocal.one_sub_pow_le_nat_mul line 101
11. lemma OAI.HoneycombLocal.sum_tail_power line 113