OAI/NumberTheory/Jacobsthal/Renewal/RawInitialDelay.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.initialOddReturnJoint_endpoint line 17
2. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawInitialEndpointState line 26
3. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawInitialEndpointState_measurable line 29
4. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawInitialEven_endpoint line 32
5. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawInitialEvenCostLaw line 43
6. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawInitialEven_cost_law line 46
7. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawInitialEven_endpoint_regenerates line 56
8. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawInitialEven_uniform_exponential line 64