OAI/NumberTheory/Jacobsthal/Estimates/CanonicalCoupledHistories.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.ActualCoupledHistories.sourceTransition line 22
2. instance OAI.Erdos970.NumberTheoryLean.ActualCoupledHistories.sourceTransition_markov line 27
3. def OAI.Erdos970.NumberTheoryLean.ActualCoupledHistories.sourceHistoryLaw line 32
4. instance OAI.Erdos970.NumberTheoryLean.ActualCoupledHistories.sourceHistoryLaw_probability line 37
5. theorem OAI.Erdos970.NumberTheoryLean.ActualCoupledHistories.sourceHistoryLaw_endpoint line 42
6. theorem OAI.Erdos970.NumberTheoryLean.ActualCoupledHistories.sourceHistoryLaw_coordinate line 47
7. theorem OAI.Erdos970.NumberTheoryLean.ActualCoupledHistories.sourceHistoryLaw_prime line 52
8. theorem OAI.Erdos970.NumberTheoryLean.ActualCoupledHistories.sourceHistoryLaw_continuous line 66
9. theorem OAI.Erdos970.NumberTheoryLean.ActualSuccessfulHistories.sourceHistory_no_reset line 97
10. theorem OAI.Erdos970.NumberTheoryLean.ActualSuccessfulHistories.sourceHistory_success_good line 101
11. theorem OAI.Erdos970.NumberTheoryLean.ActualSuccessfulHistories.sourceHistory_failure_probability line 120
12. theorem OAI.Erdos970.NumberTheoryLean.CanonicalCoupledHistories.canonical_killing_image line 139
13. theorem OAI.Erdos970.NumberTheoryLean.CanonicalCoupledHistories.sourceHistoryLaw_canonical line 149
14. theorem OAI.Erdos970.NumberTheoryLean.CanonicalCoupledHistories.sourceHistoryLaw_canonical_event line 157