OAI/NumberTheory/Jacobsthal/Probability/GeometricCostLaws.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.costTransform line 14
2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.costTransform_zero line 17
3. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.costTransform_conv line 19
4. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.conv_mass line 30
5. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.convPow_costTransform line 33
6. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.renewal_costTransform line 39
7. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.unmarkedPotential line 46
8. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.unmarkedPotential_mass line 48
9. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.unmarkedPotential_isFiniteMeasure line 54
10. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.geometricMarkedCostLaw line 59
11. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.geometricMarkedCostLaw_isProbabilityMeasure line 61
12. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.geometricMarked_costTransform line 66
13. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.geometricMarked_exponential_moment line 71
14. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.conv_ae_lower line 80
15. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.convPow_ae_nonneg line 90
16. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.unmarkedPotential_ae_nonneg line 98
17. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.geometricMarked_cost_lower line 105