OAI/NumberTheory/Jacobsthal/Renewal/MarkedRenewalComparison.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedReturn_pow_isMarkovKernel line 17
2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedReturn_cumulative_cost_lintegral line 25
3. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedReturn_cumulative_cost_law line 58
4. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.potential_mono_base line 67
5. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedReturn_potential_le_full line 74
6. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedReturn_renewal_projection line 89
7. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.fullReturn_renewal_projection line 100
8. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.marked_renewal_le_full line 109
9. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.marked_renewal_cell_bound line 116