OAI/NumberTheory/Jacobsthal/Estimates/RawSuppliedPast.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.scalarHistory line 18
2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.scalarHistory_measurable line 20
3. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.scalarIncreasing line 25
4. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.scalarIncreasing_measurable line 29
5. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawExtension_scalar_step line 33
6. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawExtension_scalar_coordinate line 48
7. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawExtension_scalarIncreasing line 66
8. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawExtension_preserves_scalar line 81
9. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawEvenHit_scalarIncreasing line 90
10. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.gapValue_log_eq_gapAt line 111
11. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.record_currentExponent line 116
12. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawEvenHit_before_cutoff line 125
13. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.suppliedPastEvent line 174
14. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.suppliedPastEvent_measurable line 177
15. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.suppliedPastEvent_self line 185
16. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawExtension_preserves_suppliedPast line 188
17. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawEvenHit_retains_suppliedPast line 199