OAI/NumberTheory/Jacobsthal/Sieve/MarkedCycleFactorization.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.completedMarked_ae_regeneration line 16
2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.completedMarked_increment_law line 22
3. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.markCostProjection line 34
4. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markCostProjection_measurable line 36
5. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.jointMarkCostLaw line 39
6. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.jointMarkCostLaw_isProbabilityMeasure line 41
7. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.marked_cycle_increment_integral line 45
8. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedCycleProductExpectation line 55
9. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.finite_marked_cycle_factorization line 59