OAI/NumberTheory/Jacobsthal/Paths/HistoryRestrictionAlgebra.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.pathPairEval line 15
2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.pathPairEval_measurable line 18
3. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.finitePath_two_trace line 22
4. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourcePair_canonical_history line 47
5. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.nextPairEval line 64
6. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.nextPairEval_measurable line 67
7. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.conditional_pair_trace_extension line 71
8. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.conditional_pair_trace line 97
9. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourcePair_after_history line 107
10. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.restriction_comp_of_retained_prefix line 124
11. abbrev OAI.Erdos970.Erdos970Dependency.MarkedVisits.RawHistory line 154
12. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawPrefix line 156
13. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawPrefix_measurable line 159
14. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawExtension line 162
15. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawExtension_isMarkovKernel line 165
16. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawExtension_retains_prefix line 180
17. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawExtension_restrict_comp line 189