OAI/NumberTheory/Jacobsthal/Renewal/RegenerationInputPotential.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.regenerationInput line 15
2. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.nonregenerationInput line 16
3. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.regenerationInput_isFiniteKernel line 18
4. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.nonregenerationInput_isFiniteKernel line 19
5. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.regenerationInput_after_pair line 21
6. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.nonregenerationInput_after_pair line 25
7. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.returnLaw_potential line 29
8. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.hitOrReturn_input_split line 31
9. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.hitOrReturn_eq_input_potential line 40