OAI/NumberTheory/Jacobsthal/Probability/SourceMarkedWords.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceCycleInputSignature line 15
2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceCycleInputSignature_measurable line 18
3. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceWordUpdate line 30
4. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceWordUpdate_measurable line 33
5. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceContinuationInput line 38
6. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceContinuationInput_measurable line 40
7. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceMarkedWordKernel line 43
8. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceMarkedWordKernel_isFiniteKernel line 50
9. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceMarkedWord_cons_lintegral line 55
10. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceBranchWitness_mass_le_one line 67
11. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceMarkedWord_mass_le_one line 71