OAI/NumberTheory/Jacobsthal/Estimates/RepeatedStepRowBound.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.RepeatedStepRowBound.repeatDensityConstant line 22
2. theorem OAI.Erdos970.NumberTheoryLean.RepeatedStepRowBound.repeatDensityConstant_pos line 24
3. def OAI.Erdos970.NumberTheoryLean.RepeatedStepRowBound.repeatBudget line 27
4. def OAI.Erdos970.NumberTheoryLean.RepeatedStepRowBound.nextRepeat line 32
5. theorem OAI.Erdos970.NumberTheoryLean.RepeatedStepRowBound.nextRepeat_measurable line 38
6. def OAI.Erdos970.NumberTheoryLean.RepeatedStepRowBound.goodRepeatNext line 45
7. theorem OAI.Erdos970.NumberTheoryLean.RepeatedStepRowBound.goodRepeatNext_measurable line 49
8. theorem OAI.Erdos970.NumberTheoryLean.RepeatedStepRowBound.good_repeat_next_row line 57