OAI/NumberTheory/Jacobsthal/Probability/MarkedCostSublaws.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceCycleLaw line 16
2. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceCycleLaw_isProbabilityMeasure line 18
3. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceMarkSet line 22
4. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceMarkSet_measurable line 24
5. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceCostProjection line 27
6. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceCostProjection_measurable line 29
7. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceCycle_cost_projection line 32
8. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceCycle_mark_mass line 37
9. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedCostLaw line 40
10. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.unmarkedCostLaw line 43
11. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedCostLaw_isFiniteMeasure line 46
12. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.unmarkedCostLaw_isFiniteMeasure line 50
13. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedCostLaw_add_unmarked line 54
14. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedCostLaw_mass line 61
15. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.unmarkedCostLaw_mass line 66
16. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedCostLaw_le line 71
17. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.unmarkedCostLaw_le line 75
18. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.source_marked_cost_lower line 79
19. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.source_unmarked_cost_lower line 82
20. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.source_marked_exponential_moments line 85