OAI/NumberTheory/Jacobsthal/Renewal/LastCycleRecord.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.lastCycleRecord line 16
2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.lastCycleRecord_measurable line 21
3. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.lastCycleRecord_cost line 26
4. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceRecordKernel line 32
5. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceRecordKernel_isFiniteKernel line 35
6. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceRecordKernel_apply line 39
7. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceRecordKernel_lintegral line 47
8. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceLastRecord_lintegral line 53
9. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceLastRecord_law line 83